From 698da3dd240ab563ee334ce54b06089d32133773 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Tue, 24 Nov 2020 10:57:17 +0100
Subject: [PATCH] intermediate session with Macro-Bug.

---
 examples/CENELEC_50128/mini_odo/mini_odo.thy   | 18 ++++++++++++------
 .../scholarly_paper/2020-iFM-CSP/paper.thy     | 10 +++++-----
 2 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy
index 6216bbc..1d9da10 100755
--- a/examples/CENELEC_50128/mini_odo/mini_odo.thy
+++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy
@@ -443,13 +443,13 @@ integrated source, we will, in the following, point out three scenarios.\<close>
 
 subsection\<open>Internal Verification of Claims in the Requirements Specification.\<close>
 text\<open>In our case, the SR-team early on detected a property necessary
-for error-detection of the device (c.f. @{docitem verific}):
+for error-detection of the device (c.f. @{technical verific}):
 \enlargethispage{2\baselineskip}\begin{isar}
 text*[encoder_props::requirement]<open> The requirement specification team ...
     C1 & C2 & C3  = 0   (bitwise logical AND operation)
     C1 | C2 | C3  = 1   (bitwise logical OR operation) <close>
 \end{isar}
-After the Isabelle proofs shown in @{docitem verific}, we can either register the theorems
+After the Isabelle proofs shown in @{technical verific}, we can either register the theorems
 directly in an evidence statement: 
 
 \begin{isar}
@@ -562,13 +562,19 @@ to a test-environment or test-engine. \<close>
 
 text\<open>Finally some examples of references to doc-items, i.e. text-elements with declared 
      meta-information and status. \<close> 
-text \<open> As established by @{docitem (unchecked) \<open>t10\<close>}, 
-                         @{docitem (define) \<open>t10\<close>} \<close>
-text \<open> the               @{docitem \<open>t10\<close>}                      
-       as well as the    @{docitem \<open>ass122\<close>}\<close>  
+text \<open> As established by @{test_result (unchecked) \<open>t10\<close>}, 
+                         @{test_result (define) \<open>t10\<close>} \<close>
+text \<open> the               @{test_result \<open>t10\<close>}                      
+       as well as the    @{SRAC \<open>ass122\<close>}\<close>  
 text \<open> represent a justification of the safety related applicability 
        condition @{SRAC \<open>ass122\<close>} aka exported constraint @{EC \<open>ass122\<close>}.\<close> 
 
+(* due to notational conventions for antiquotations, one may even write: *)
+(* CRASHES WITH LaTeX backend error. *)
+text \<open> represent a justification of the safety related applicability 
+       condition \<^SRAC>\<open>ass122\<close> aka exported constraint \<^EC>\<open>ass122\<close>.\<close> 
+
+
 (*<*)   
 end
 (*>*)
diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy
index e4563d1..3302e56 100644
--- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy
+++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy
@@ -527,16 +527,16 @@ To handle termination better, we added two new processes \<open>CHAOS\<^sub>S\<^
 %Note that we do not redefine \<open>RUN\<close> with \<open>SKIP\<close> because this process is supposed to never terminate, 
 %thus must be without it. 
 \<close>
-(*
-Definition*[X22]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                       \<^vs>\<open>-0.7cm\<close>\<close>
-Definition*[X32]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>          \<^vs>\<open>-0.7cm\<close>\<close>
-Definition*[X42]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<^vs>\<open>-0.7cm\<close>\<close>
+
+text*[X22::"definition"]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                       \<close>
+text*[X32::"definition"]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>         \<close>
+Definition*[X42::"definition"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<close>
 
 text\<open> The \<open>RUN\<close>-process defined @{definition X22} represents the process that accepts all 
 events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in 
 @{definition X32} and @{definition X42}: the process that non-deterministically stops or 
 accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionally terminate.\<close>
-*)
+
 
 Definition*[X2]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                       \<^vs>\<open>-0.7cm\<close>\<close>
 Definition*[X3]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>          \<^vs>\<open>-0.7cm\<close>\<close>