diff -r 8bb064045b4e -r e51c9a67a68d thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Paper/Paper.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -15,13 +15,20 @@
 abbreviation 
  "ders_syn r s \<equiv> ders s r"
 
+(*
 notation (latex output)
-  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10)
+*)
+(*
+notation (latex output)
   Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and  
+*)
 
+(*
+notation (latex output)
   ZERO ("\<^bold>0" 78) and 
   ONE ("\<^bold>1" 78) and 
-  CHAR ("_" [1000] 80) and
+  CH ("_" [1000] 80) and
   ALT ("_ + _" [77,77] 78) and
   SEQ ("_ \<cdot> _" [77,77] 78) and
   STAR ("_\<^sup>\<star>" [1000] 78) and
@@ -55,9 +62,13 @@
   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and
   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
   slexer ("lexer\<^sup>+" 1000) and
+*)
 
+(*
+notation (latex output)
   ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and
   ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)
+*)
 
 definition 
   "match r s \<equiv> nullable (ders s r)"
@@ -226,7 +237,7 @@
   @{text "r :="}
   @{const "ZERO"} $\mid$
   @{const "ONE"} $\mid$
-  @{term "CHAR c"} $\mid$
+  @{term "CH c"} $\mid$
   @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$
   @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$
   @{term "STAR r"} 
@@ -405,7 +416,7 @@
   @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm]
   @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[4mm]
   @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad  
-  @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}
+  %%@ { thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}
   \end{tabular}
   \end{center}
 
@@ -1024,20 +1035,9 @@
 
 \begin{center}  
 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}	
-@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &
-@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\
-
-@{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\,(A1) &
-@{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\,(A2)\smallskip\\
+??? &
+??? \smallskip\\
 
-@{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}\,(A3) &
-@{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\,(A4)\smallskip\\
-
-@{thm[mode=Rule] K1[of "v" "vs" "r"]}\,(K1) &
-@{thm[mode=Rule] K2[of "v" "vs" "r"]}\,(K2)\smallskip\\
-
-@{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\,(K3) &
-@{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\,(K4)
 \end{tabular}
 \end{center}
 
@@ -1062,7 +1062,9 @@
   What is interesting for our purposes is that the properties reflexivity,
   totality and transitivity for this GREEDY ordering can be proved
   relatively easily by induction.
+*}
 
+(*
   These properties of GREEDY, however, do not transfer to the POSIX
   ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. 
   To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is
@@ -1071,7 +1073,9 @@
   >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)
   (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
   formulation, for example:
+*)
 
+text {*
   \begin{falsehood}
   Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}.
   If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}