Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF

Isabelle_DOF/ROOT

@@ -46,11 +46,11 @@ session "Isabelle_DOF" (AFP) = "Functional-Automata" +
     "figures/definition-use-CSP-pdf.png"
     "figures/definition-use-CSP.png"
     "figures/MyCommentedIsabelle.png"
-    "figures/doc-mod-generic.png"
-    "figures/doc-mod-isar.png"
-    "figures/doc-mod-onto-docinst.png"
-    "figures/doc-mod-DOF.png"
-    "figures/doc-mod-term-aq.png"
+    "figures/doc-mod-generic.pdf"
+    "figures/doc-mod-isar.pdf"
+    "figures/doc-mod-onto-docinst.pdf"
+    "figures/doc-mod-DOF.pdf"
+    "figures/doc-mod-term-aq.pdf"
   export_classpath
 
 

Isabelle_DOF/thys/manual/M_02_Background.thy

@@ -106,9 +106,9 @@ text\<open>
 
 side_by_side_figure*[docModGenConcr::side_by_side_figure,anchor="''docModGen''",
                       caption="''Schematic Representation.''",relative_width="45",
-                      src="''figures/doc-mod-generic.png''",anchor2="''docModIsar''",
+                      src="''figures/doc-mod-generic.pdf''",anchor2="''docModIsar''",
                       caption2="''The Isar Instance.''",relative_width2="45",
-                      src2="''figures/doc-mod-isar.png''"]\<open>A Representation of a Document Model.\<close>
+                      src2="''figures/doc-mod-isar.pdf''"]\<open>A Representation of a Document Model.\<close>
 
 text\<open>The body of a theory file consists of a sequence of \<^emph>\<open>commands\<close> that must be introduced
 by a command keyword such as \<^boxed_theory_text>\<open>requirement\<close> above. Command keywords may mark 
@@ -184,9 +184,9 @@ text\<open>Antiquotations seen as semantic macros are partial functions of type
 
 side_by_side_figure*[docModOnto::side_by_side_figure,anchor="''docModGen''",
                       caption="''A Document with Ontological Annotations.''",relative_width="47",
-                      src="''figures/doc-mod-DOF.png''",anchor2="''docModDOF''",
+                      src="''figures/doc-mod-DOF.pdf''",anchor2="''docModDOF''",
                       caption2="''Ontological References.''",relative_width2="47",
-                      src2="''figures/doc-mod-onto-docinst.png''"]\<open>Documents conform to Ontologies.\<close>
+                      src2="''figures/doc-mod-onto-docinst.pdf''"]\<open>Documents conform to Ontologies.\<close>
 
 text\<open>Since Isabelle's commands are freely programmable, it is possible to implement  \<^dof> as an 
 extension of the system. In particular, the ontology language of \<^dof> provides an  ontology 

Isabelle_DOF/thys/manual/M_03_GuidedTour.thy

@@ -527,7 +527,7 @@ ontologically checked prior arguments \<open>arg\<^sub>1 ... arg\<^sub>n\<^sub>-
 process; ontologically, they can be used to assure the traceability of, \<^eg>, semi-formal 
 assumptions throughout their way to formalisation and use in lemmas and proofs. \<close> 
 
-figure*[doc_termAq::figure,relative_width="50",src="''figures/doc-mod-term-aq.png''"]
+figure*[doc_termAq::figure,relative_width="50",src="''figures/doc-mod-term-aq.pdf''"]
                       \<open>Term-Antiquotations Referencing to Annotated Elements\<close>
 text\<open>As shown in @{figure \<open>doc_termAq\<close>}, this feature of  \<^isadof> substantially increases
 the expressibility of links between the formal and the informal in \<^dof> documents.\<close>