Merge branch 'main' into isabelle_nightly

Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy

@@ -82,12 +82,12 @@ which will appear textually later. With this pragmatics, an "out-of-    order-pr
 can be achieved within \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close> for the most common cases.\<close>
 
 
-
+(*<*) (* PDF references to definition* not implemented *)
 Definition*[e1bis::"definition", short_name="\<open>Nice lemma.\<close>"]
    \<open>Lorem ipsum dolor sit amet, ... 
     This is formally defined as follows in @{definition (unchecked) "e1bisbis"}\<close>
 definition*[e1bisbis, status=formal] e :: int where "e = 2"
-
+(*>*)
 section\<open>Tests for Theorems, Assertions, Assumptions, Hypothesis, etc.\<close>
 
 declare [[Theorem_default_class     = "theorem",
@@ -127,12 +127,13 @@ Corollary*[d5]\<open>"Freeform Corollary"\<close>
 
 Consequence*[d6::scholarly_paper.consequence]\<open>"Freeform Consequence"\<close> \<comment> \<open>longname just for test\<close>
 
+(*<*)
 declare_reference*[ababa::scholarly_paper.assertion]
 Assertion*[d7]\<open>Freeform Assumption with forward reference to the formal  
                @{assertion (unchecked) ababa}.\<close>  
 assert*[ababa::assertion] "3 < (4::int)"
 assert*[ababab::assertion] "0 < (4::int)"
-
+(*>*)
 
 Conclusion*[d8]\<open>"Freeform Conclusion"\<close>
 

Isabelle_DOF-Unit-Tests/COL_Test.thy

@@ -31,12 +31,12 @@ section\<open>General Figure COL Elements\<close>
 figure*[fig1_test,relative_width="95",file_src="''figures/A.png''"]
        \<open> This is the label text  \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<close>  
 
-(*<*)
+(*<*) (* text* with type figure not supported *)
 text*[fig2_test::figure, relative_width="95",file_src="''figures/A.png''"
 ]\<open> This is the label text\<close>
-(*>*)
-text\<open>check @{figure fig1_test} cmp to @{figure fig2_test}\<close>
 
+text\<open>check @{figure fig1_test} cmp to @{figure fig2_test}\<close>
+(*>*)
 
 
 (* And a side-chick ... *)

Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy

@@ -37,6 +37,7 @@ text\<open> This uses elements of two ontologies, notably
       \<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> and \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>.\<close>
 
 (*<*)
+
 title*[ag::title, short_title="Some\<open>ooups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
 subtitle*[af::subtitle, abbrev = "Some\<open>ooups-oups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
 chapter*[a0::A, x = "3"]   \<open> Lorem ipsum dolor sit amet ... \<close>
@@ -48,11 +49,9 @@ subsubsection*[ac::A, x = "3"]  \<open> Lorem ipsum dolor sit amet, ...
                                                                           ontological instances 
                                                                           assigned to text 
                                                                           elements ...\<close>
-(*>*)
 
 
 text\<open>Meta-Objects are typed, and references have to respect this : \<close>
-(*<*)
 text-assert-error[ad]\<open> \<^title>\<open>a\<close> \<close>    \<open>reference ontologically inconsistent\<close>
 text-assert-error[ae]\<open> \<^title>\<open>af\<close> \<close>\<open>reference ontologically inconsistent\<close> 
                        \<comment> \<open>erroneous reference: please consider class hierarchy!\<close>
@@ -116,17 +115,17 @@ definition*[e6::E] facu :: "nat \<Rightarrow> nat" where "facu arg = undefined"
 text\<open>As shown in @{E \<open>e5\<close>} following from  @{E \<open>e6\<close>}\<close> 
 
 
-(*>*)
 text\<open>As shown in @{C \<open>c4\<close>}\<close>
+(*>*)
 
 
 
 text\<open>Ontological information ("class instances") is mutable: \<close>
 
 update_instance*[d::D, a1 := X2]
-
+(*<*)
 text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>} ... \<close> \<comment> \<open>untyped or typed referencing \<close>
-
+(*>*)
 text-assert-error[ae::text_element]\<open>the function @{C [display] "c4"} \<close>\<open>referred text-element is no macro!\<close>
 
 text*[c2::C, x = "\<open>delta\<close>"]  \<open> ... in ut tortor eleifend augue pretium consectetuer.  \<close>
@@ -141,9 +140,9 @@ theorem some_proof : "True" by simp
 
 text\<open>This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\<close>
 update_instance*[f::F,r:="[@{thm ''Concept_OntoReferencing.some_proof''}]"]
-
+(*<*)
 text\<open> ..., mauris amet, id elit aliquam aptent id,  ... @{docitem \<open>a\<close>} \<close>
-
+(*>*)
 text\<open>Here we add and maintain a link that is actually modeled as m-to-n relation ...\<close>
 update_instance*[f::F,b:="{(@{docitem  \<open>a\<close>}::A,@{docitem  \<open>c1\<close>}::C), 
                            (@{docitem  \<open>a\<close>},   @{docitem  \<open>c2\<close>})}"] 

Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy

@@ -28,14 +28,14 @@ proof elements. Some tests cover also the critical cases concerning name spaces
 
 
 section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
-
+(*<*)
 ML*[thefunction::B,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
                                val t = \<^value_>\<open>x @{B \<open>thefunction\<close>}\<close>\<close>
 ML\<open>fac 5; t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the 
                  resulting toplevel state is preserved.\<close>
 text*[the::C]\<open> @{B "thefunction"} \<close>
-
 text\<open>... and here we reference @{B \<open>thefunction\<close>}.\<close>
+(*>*)
 
 
 
@@ -65,7 +65,7 @@ of the current implementation.
 \<close>
 
 section\<open>Term Annotation evaluation\<close>
-
+(*<*)
 text\<open>We can validate a term with TA:\<close>
 term*[axx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close>
 
@@ -80,7 +80,7 @@ value*\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>syntax che
 value*[axxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>defining a reference of class A\<close> 
 
 text\<open>check : @{A "axxx"}\<close> \<comment> \<open>using it\<close> 
-
+(*>*)
 text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
 It is a concept which will be used to implement an ontology. It has roughly the same meaning as
 an individual in an OWL ontology.
@@ -158,6 +158,7 @@ value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances} = [@{Z
 text\<open>Now, we want to get all the instances of the @{doc_class A}\<close>
 value*\<open>@{A-instances}\<close>
 
+(*<*)
 text\<open>Warning: If you make a request on attributes that are undefined in some instances,
 you will get a result which includes these unresolved cases.
 In the following example, we request the instances of the @{doc_class A}.
@@ -166,7 +167,7 @@ whose our theory inherits from, and this docitem instance does not initialize it
 So in the request result we get an unresolved case because the evaluator can not get
 the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>sdf\<close>}:\<close>
 value*\<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
-
+(*>*)
 section\<open>Limitations\<close>
 
 text\<open>There are still some limitations.
@@ -216,9 +217,10 @@ assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>
 term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
 assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
 
+(*<*)
 text*[assertionAA::A]\<open>@{A "assertionA"}\<close> 
 text\<open>... and here we reference @{A \<open>assertionA\<close>}.\<close>
-
+(*>*)
 assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
 
 text\<open>The optional evaluator of \<open>value*\<close> and \<open>assert*\<close> must be specified after the meta arguments:\<close>

Isabelle_DOF-Unit-Tests/Latex_Tests.thy

@@ -39,12 +39,11 @@ text\<open>Pythons ReStructuredText (RST).
     \<close>
 
 text*[aaaa::B]\<open>dfg @{thm [display] refl}\<close>
-                            
+(*<*)                            
 text-[dfgdfg::B]
 \<open> Lorem ipsum ...  @{thm [display] refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
 
 text-latex\<open> Lorem ipsum ...  @{thm [display] refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
-
 text-[asd::B]
 \<open>... and here is its application macro expansion: 
      @{B [display] "dfgdfg"} 
@@ -76,6 +75,7 @@ text-latex\<open> \<^theory_text>\<open>definition df = ...
        @{theory_text [display] \<open>definition df = ... \<lambda>x.  
                                \<close>}
        @{cartouche [display]   \<open> @{figure "cfgdfg"}\<close>} \<close>
+(*>*)
 
 text\<open>Final Status:\<close>
 print_doc_items