forked from Isabelle_DOF/Isabelle_DOF
Milestone reached:
- further debugging - all tests checked - all examples running (after updates to current attribute conventions)
This commit is contained in:
parent
cedac17646
commit
0f36e8b761
|
@ -393,7 +393,9 @@ fun print_doc_items b ctxt =
|
||||||
writeln (" type: "^cid);
|
writeln (" type: "^cid);
|
||||||
writeln (" origine: "^thy_name);
|
writeln (" origine: "^thy_name);
|
||||||
writeln (" value: " ^ (Syntax.string_of_term ctxt value))
|
writeln (" value: " ^ (Syntax.string_of_term ctxt value))
|
||||||
);
|
)
|
||||||
|
| print_item (n, NONE) =
|
||||||
|
(writeln ("forward reference for docitem: "^n));
|
||||||
in map print_item (Symtab.dest x);
|
in map print_item (Symtab.dest x);
|
||||||
writeln "=====================================\n\n\n" end;
|
writeln "=====================================\n\n\n" end;
|
||||||
|
|
||||||
|
|
|
@ -19,8 +19,6 @@ text\<open> @{thm refl} of name @{thm [source] refl}
|
||||||
|
|
||||||
|
|
||||||
section{* Example *}
|
section{* Example *}
|
||||||
print_doc_classes
|
|
||||||
print_doc_items
|
|
||||||
|
|
||||||
text*[tralala] {* Brexit means Brexit *}
|
text*[tralala] {* Brexit means Brexit *}
|
||||||
|
|
||||||
|
@ -53,6 +51,10 @@ declare_reference* [lalala::requirement, alpha="main", beta=42]
|
||||||
|
|
||||||
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
||||||
|
|
||||||
|
print_doc_classes
|
||||||
|
print_doc_items
|
||||||
|
|
||||||
|
|
||||||
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -37,7 +37,7 @@ text{*
|
||||||
|
|
||||||
|
|
||||||
text*[exo1 :: Exercise,
|
text*[exo1 :: Exercise,
|
||||||
Exercise.concerns= "{setter,student,checker,externalExaminer}"]
|
concerns= "{setter,student,checker,externalExaminer}"]
|
||||||
{* On considère la fonction h définie sur l’intervalle [0..+\<infinity>] par :
|
{* On considère la fonction h définie sur l’intervalle [0..+\<infinity>] par :
|
||||||
@{term "h(x) = x * exponent (-x)"}
|
@{term "h(x) = x * exponent (-x)"}
|
||||||
*}
|
*}
|
||||||
|
@ -46,7 +46,7 @@ definition h :: "real \<Rightarrow> real"
|
||||||
where "h x \<equiv> x * exp (- x)"
|
where "h x \<equiv> x * exp (- x)"
|
||||||
|
|
||||||
|
|
||||||
text*[q1::Task, Task.concerns= "{setter,student}",
|
text*[q1::Task, concerns= "{setter,student}",
|
||||||
level="oneStar", mark="1::int", type="formal"]
|
level="oneStar", mark="1::int", type="formal"]
|
||||||
{* Déterminer la limite de la fonction @{term h} en +\<infinity>. *}
|
{* Déterminer la limite de la fonction @{term h} en +\<infinity>. *}
|
||||||
|
|
||||||
|
@ -57,7 +57,7 @@ lemma q1 : "(h \<longlongrightarrow> (0::real)) at_top" sorry
|
||||||
text*[v1::Validation, proofs="[@{thm ''q1''}::thm]"] {* See lemma @{thm q1}. *}
|
text*[v1::Validation, proofs="[@{thm ''q1''}::thm]"] {* See lemma @{thm q1}. *}
|
||||||
|
|
||||||
|
|
||||||
text*[q2::Task, Task.concerns= "{setter,checker,student}",
|
text*[q2::Task, concerns= "{setter,checker,student}",
|
||||||
level="oneStar", mark="1::int", type="formal"]
|
level="oneStar", mark="1::int", type="formal"]
|
||||||
{* Étudier les variations de la fonction @{term h} sur l'intervalle [0..+\<infinity>] et
|
{* Étudier les variations de la fonction @{term h} sur l'intervalle [0..+\<infinity>] et
|
||||||
dresser son tableau de variation *}
|
dresser son tableau de variation *}
|
||||||
|
@ -90,7 +90,7 @@ text*[v2::Validation, proofs="[@{thm ''q2_b''}, @{thm ''q2_c''}]"]
|
||||||
{* See lemmas @{thm q2_b} and @{thm q2_c}. *}
|
{* See lemmas @{thm q2_b} and @{thm q2_c}. *}
|
||||||
|
|
||||||
|
|
||||||
text*[q3a::Task, Task.concerns= "{setter,checker,student}",
|
text*[q3a::Task, concerns= "{setter,checker,student}",
|
||||||
level="oneStar", mark="1::int", type="formal"]
|
level="oneStar", mark="1::int", type="formal"]
|
||||||
{* Vérifier que pour tout nombre réel x appartenant à l'intervalle [0..+\<infinity>], on a :
|
{* Vérifier que pour tout nombre réel x appartenant à l'intervalle [0..+\<infinity>], on a :
|
||||||
@{term "h x = (exp (- x)) - (h' x)"}. *}
|
@{term "h x = (exp (- x)) - (h' x)"}. *}
|
||||||
|
@ -106,8 +106,8 @@ subsubsection*[v3a::Validation, proofs="[@{thm ''q3a''}::thm]"]
|
||||||
|
|
||||||
|
|
||||||
subsection*[sol1 :: Solution,
|
subsection*[sol1 :: Solution,
|
||||||
Solution.content="[exo1::Exercise]",
|
content="[exo1::Exercise]",
|
||||||
Solution.valids = "[v1::Validation,v2,v3a]"]
|
valids = "[v1::Validation,v2,v3a]"]
|
||||||
{* See validations. *}
|
{* See validations. *}
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -36,7 +36,7 @@ figure*[figure::figure, spawn_columns=False,relative_width="''80''",
|
||||||
\<open>A Polynome.\<close>
|
\<open>A Polynome.\<close>
|
||||||
|
|
||||||
|
|
||||||
subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\<open>Exercise 1\<close>
|
subsubsection*[exo1 :: Exercise, content="[q1::Task,q2::Task]"]\<open>Exercise 1\<close>
|
||||||
text{*
|
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}
|
||||||
|
@ -48,7 +48,7 @@ Here are the first four lines of a number pattern.
|
||||||
*}
|
*}
|
||||||
|
|
||||||
declare [[show_sorts=false]]
|
declare [[show_sorts=false]]
|
||||||
subsubsection*[exo2 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\<open>Exercise 2\<close>
|
subsubsection*[exo2 :: Exercise, content="[q1::Task,q2::Task]"]\<open>Exercise 2\<close>
|
||||||
|
|
||||||
text{* Find the roots of the polynome:
|
text{* Find the roots of the polynome:
|
||||||
@{term "(x^3) - 6 * x^2 + 5 * x + 12"}.
|
@{term "(x^3) - 6 * x^2 + 5 * x + 12"}.
|
||||||
|
@ -95,7 +95,7 @@ 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>
|
subsubsection*[exo3 :: 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
|
||||||
|
|
|
@ -93,7 +93,7 @@ we discuss the user-interaction generated from the ontological definitions. Fin
|
||||||
conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. \<close>
|
conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. \<close>
|
||||||
|
|
||||||
section*[bgrnd::text_section,
|
section*[bgrnd::text_section,
|
||||||
text_section.main_author="Some(@{docitem ''adb''}::author)"]
|
main_author="Some(@{docitem ''adb''}::author)"]
|
||||||
\<open> Background: The Isabelle System \<close>
|
\<open> Background: The Isabelle System \<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
While Isabelle is widely perceived as an interactive theorem prover
|
While Isabelle is widely perceived as an interactive theorem prover
|
||||||
|
@ -166,7 +166,7 @@ Isabelle's PIDE offers auto-completion and error-messages while typing the above
|
||||||
\emph{semi-formal} content. \<close>
|
\emph{semi-formal} content. \<close>
|
||||||
|
|
||||||
section*[isadof::text_section,
|
section*[isadof::text_section,
|
||||||
text_section.main_author="Some(@{docitem ''adb''}::author)"]
|
main_author="Some(@{docitem ''adb''}::author)"]
|
||||||
\<open> \isadof \<close>
|
\<open> \isadof \<close>
|
||||||
|
|
||||||
text\<open> An \isadof document consists of three components:
|
text\<open> An \isadof document consists of three components:
|
||||||
|
|
|
@ -4,7 +4,7 @@ begin
|
||||||
|
|
||||||
open_monitor*[struct::M]
|
open_monitor*[struct::M]
|
||||||
|
|
||||||
section*[a::A, x = "''alpha''"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
||||||
|
|
||||||
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue