forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
b38297afe1
|
@ -20,14 +20,13 @@ subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
*}
|
*}
|
||||||
|
|
||||||
|
(* should be in DOF-core *)
|
||||||
(*
|
(*
|
||||||
text*[fig1::figure, width = "Some(textwidth 80)",
|
figure*[figure::figure, spawn_columns=False,relative_width="''80''",
|
||||||
"file"="@{file ''../../../figures/Dogfood-Intro.png''}"]
|
src="''figures/Polynomialdeg5.png''"] \<open> A Polynome. \<close>
|
||||||
{* Ouroboros I : This paper from inside ... *}
|
|
||||||
*)
|
*)
|
||||||
|
subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\<open>Exercise 1\<close>
|
||||||
subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]
|
text{*
|
||||||
{*
|
|
||||||
Here are the first four lines of a number pattern.
|
Here are the first four lines of a number pattern.
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item Line 1 : @{term "1*6 + 2*4 = 2*7"}
|
\item Line 1 : @{term "1*6 + 2*4 = 2*7"}
|
||||||
|
@ -37,6 +36,26 @@ Here are the first four lines of a number pattern.
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
*}
|
*}
|
||||||
|
|
||||||
|
declare [[show_sorts=false]]
|
||||||
|
subsubsection*[exo2 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\<open>Exercise 2\<close>
|
||||||
|
|
||||||
|
text{* Find the roots of the polynome:
|
||||||
|
@{term "(x^3) - 6 * x^2 + 5 * x + 12"}.
|
||||||
|
Note the intermediate steps in the following fields and submit the solution. *}
|
||||||
|
text{*
|
||||||
|
\begin{Form}[action={http://your-web-server.com/path/receiveform.cgi}]
|
||||||
|
\begin{tabular}{l}
|
||||||
|
From @{term "(x^3) - 6 * x^2 + 5 * x + 12"} \\\\
|
||||||
|
\TextField{have 1} \\\\
|
||||||
|
\TextField{have 2} \\\\
|
||||||
|
\TextField{have 3} \\\\
|
||||||
|
\TextField{finally show} \\\\
|
||||||
|
\CheckBox[width=1em]{Has the polynomial as many solutions as its degree ? } \\\\
|
||||||
|
\Submit{Submit}\\
|
||||||
|
\end{tabular}
|
||||||
|
\end{Form}
|
||||||
|
*}
|
||||||
|
|
||||||
(* a bit brutal, as long as lemma* does not yet work *)
|
(* a bit brutal, as long as lemma* does not yet work *)
|
||||||
(*<*)
|
(*<*)
|
||||||
lemma check_polynome :
|
lemma check_polynome :
|
||||||
|
@ -65,6 +84,8 @@ text*[a4::Answer_Formal_Step]{* Next Step: Fill in term and justification *}
|
||||||
text*[q1::Task, level="oneStar", mark="1::int", type="formal"]
|
text*[q1::Task, level="oneStar", mark="1::int", type="formal"]
|
||||||
{* Complete Line 10 : @{term "10*x + 2*y = 11*16"} *}
|
{* Complete Line 10 : @{term "10*x + 2*y = 11*16"} *}
|
||||||
|
|
||||||
|
subsubsection*[exo3 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\<open>Exercise 3\<close>
|
||||||
|
|
||||||
text*[q2::Task, level="threeStars", mark="3::int", type="formal"]
|
text*[q2::Task, level="threeStars", mark="3::int", type="formal"]
|
||||||
{*
|
{*
|
||||||
Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers
|
Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers
|
||||||
|
|
Binary file not shown.
After Width: | Height: | Size: 4.9 KiB |
|
@ -26,6 +26,8 @@ doc_class Author =
|
||||||
affiliation :: "string"
|
affiliation :: "string"
|
||||||
email :: "string"
|
email :: "string"
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
datatype Subject =
|
datatype Subject =
|
||||||
algebra | geometry | statistical | analysis
|
algebra | geometry | statistical | analysis
|
||||||
|
|
||||||
|
@ -45,6 +47,15 @@ doc_class Header =
|
||||||
doc_class Exam_item =
|
doc_class Exam_item =
|
||||||
concerns :: "ContentClass set"
|
concerns :: "ContentClass set"
|
||||||
|
|
||||||
|
(* should go into something more fundamental on texts. *)
|
||||||
|
datatype placement = h | t | b | ht | hb
|
||||||
|
doc_class figure = Exam_item +
|
||||||
|
relative_width :: "string" (* percent of textwidth *)
|
||||||
|
src :: "string"
|
||||||
|
placement :: placement
|
||||||
|
spawn_columns :: bool <= True
|
||||||
|
|
||||||
|
|
||||||
type_synonym SubQuestion = string
|
type_synonym SubQuestion = string
|
||||||
|
|
||||||
doc_class Answer_Formal_Step = Exam_item +
|
doc_class Answer_Formal_Step = Exam_item +
|
||||||
|
|
Loading…
Reference in New Issue