From e9044e8d5a25a0f53b66d47f15d3a2cb73a915fa Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Fri, 12 May 2023 17:50:42 +0200
Subject: [PATCH] Updating odo

---
 .../CENELEC_50128/mini_odo/mini_odo.thy       |  4 +--
 .../TR_MyCommentedIsabelle.thy                | 25 ++++++++-----------
 2 files changed, 12 insertions(+), 17 deletions(-)

diff --git a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy
index f36e004..0495e10 100644
--- a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy
+++ b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy
@@ -126,7 +126,7 @@ text\<open>
 
 subsection\<open>Capturing ``System Architecture.''\<close>
 
-figure*["three-phase"::figure,relative_width="70",src="''figures/three-phase-odo''"]
+figure*["three-phase"::figure,relative_width="70",file_src="''figures/three-phase-odo.pdf''"]
 \<open>An odometer with three sensors \<open>C1\<close>, \<open>C2\<close>, and \<open>C3\<close>.\<close>
 
 text\<open>
@@ -162,7 +162,7 @@ text\<open>
   of the measuring device, and the required format and precision of the measurements of the odometry
   function as represented (see @{figure (unchecked) "df-numerics-encshaft"}).\<close>
 
-figure*["df-numerics-encshaft"::figure,relative_width="76",src="''figures/df-numerics-encshaft''"]
+figure*["df-numerics-encshaft"::figure,relative_width="76",file_src="''figures/df-numerics-encshaft.png''"]
 \<open>Real distance vs. discrete distance vs. shaft-encoder sequence\<close>
 
 
diff --git a/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
index d1702f7..a80b722 100644
--- a/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
+++ b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
@@ -79,7 +79,7 @@ text\<open> \<^vs>\<open>-0.5cm\<close>
   maximum of formal content which makes this text re-checkable at each load and easier 
   maintainable. \<close>
 
-figure*[architecture::figure,relative_width="70",src="''figures/isabelle-architecture''"]\<open> 
+figure*[architecture::figure,relative_width="70",file_src="''figures/isabelle-architecture.pdf''"]\<open> 
      The system architecture of Isabelle (left-hand side) and the  asynchronous communication 
      between the Isabelle system and the IDE (right-hand side). \<close>
 
@@ -148,7 +148,7 @@ text\<open> \<open>*\<open>This is a text.\<close>\<close>\<close>
 
 text\<open>and displayed in the Isabelle/jEdit front-end at the sceen by:\<close>
 
-figure*[fig2::figure, relative_width="60", placement="pl_h", src="''figures/text-element''"]
+figure*[fig2::figure, relative_width="60", file_src="''figures/text-element.pdf''"]
         \<open>A text-element as presented in Isabelle/jEdit.\<close>
 
 text\<open>The text-commands, ML-commands (and in principle any other command) can be seen as 
@@ -807,18 +807,13 @@ text\<open>  They reflect the Pure logic depicted in a number of presentations s
   Notated as logical inference rules, these operations were presented as follows:
 \<close>
 
-side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-kernel1''",
-                      caption="''Pure Kernel Inference Rules I ''",relative_width="48",
-                      src="''figures/pure-inferences-I''",anchor2="''fig-kernel2''",
-                      caption2="''Pure Kernel Inference Rules II''",relative_width2="47",
-                      src2="''figures/pure-inferences-II''"]\<open>  \<close>
+text*["text-elements"::float, 
+      main_caption="\<open>Kernel Inference Rules.\<close>"]
+\<open>
+@{fig_content (width=48, caption="Pure Kernel Inference Rules I.") "figures/pure-inferences-I.pdf"
+}\<^hfill>@{fig_content (width=47, caption="Pure Kernel Inference Rules II.") "figures/pure-inferences-II.pdf"} 
+\<close>
 
-(*
-figure*[kir1::figure,relative_width="100",src="''figures/pure-inferences-I''"]
-       \<open> Pure Kernel Inference Rules I.\<close>
-figure*[kir2::figure,relative_width="100",src="''figures/pure-inferences-II''"]
-       \<open> Pure Kernel Inference Rules II. \<close>
- *)
 
 text\<open>Note that the transfer rule:
 \[
@@ -1440,7 +1435,7 @@ text\<open>The document model forsees a number of text files, which are organize
   secondary formats can be \<^verbatim>\<open>.sty\<close>,\<^verbatim>\<open>.tex\<close>, \<^verbatim>\<open>.png\<close>, \<^verbatim>\<open>.pdf\<close>, or other files processed 
   by Isabelle and listed in a configuration processed by the build system.\<close>
 
-figure*[fig3::figure, relative_width="100",src="''figures/document-model''"]
+figure*[fig3::figure, relative_width="100",file_src="''figures/document-model.pdf''"]
         \<open>A Theory-Graph in the Document Model\<close>
 
 text\<open>A \<^verbatim>\<open>.thy\<close> file consists of a \<^emph>\<open>header\<close>, a \<^emph>\<open>context-definition\<close> and
@@ -1535,7 +1530,7 @@ text\<open> ... uses the antiquotation @{ML "@{here}"} to infer from the system
   of itself in the global document, converts it to markup (a string-representation of it) and sends
   it via the usual @{ML "writeln"} to the interface. \<close>
 
-figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"]
+figure*[hyplinkout::figure,relative_width="40",file_src="''figures/markup-demo.png''"]
 \<open>Output with hyperlinked position.\<close>
 
 text\<open>@{figure \<open>hyplinkout\<close>} shows the produced output where the little house-like symbol in the