--- a/thys/Spec.thy	Mon Feb 22 03:22:26 2021 +0000
+++ b/thys/Spec.thy	Thu Feb 25 22:46:58 2021 +0000
@@ -3,10 +3,7 @@
   imports RegLangs
 begin
 
-
-
-
-section {* "Plain" Values *}
+section \<open>"Plain" Values\<close>
 
 datatype val = 
   Void
@@ -17,7 +14,7 @@
 | Stars "val list"
 
 
-section {* The string behind a value *}
+section \<open>The string behind a value\<close>
 
 fun 
   flat :: "val \<Rightarrow> string"
@@ -38,7 +35,7 @@
 by (induct vs) (auto)
 
 
-section {* Lexical Values *}
+section \<open>Lexical Values\<close>
 
 inductive 
   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
@@ -47,7 +44,7 @@
 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 | "\<Turnstile> Void : ONE"
-| "\<Turnstile> Char c : CHAR c"
+| "\<Turnstile> Char c : CH c"
 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 
 inductive_cases Prf_elims:
@@ -55,7 +52,7 @@
   "\<Turnstile> v : SEQ r1 r2"
   "\<Turnstile> v : ALT r1 r2"
   "\<Turnstile> v : ONE"
-  "\<Turnstile> v : CHAR c"
+  "\<Turnstile> v : CH c"
   "\<Turnstile> vs : STAR r"
 
 lemma Prf_Stars_appendE:
@@ -118,11 +115,11 @@
 
 
 
-section {* Sets of Lexical Values *}
+section \<open>Sets of Lexical Values\<close>
 
-text {*
+text \<open>
   Shows that lexical values are finite for a given regex and string.
-*}
+\<close>
 
 definition
   LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
@@ -131,7 +128,7 @@
 lemma LV_simps:
   shows "LV ZERO s = {}"
   and   "LV ONE s = (if s = [] then {Void} else {})"
-  and   "LV (CHAR c) s = (if s = [c] then {Char c} else {})"
+  and   "LV (CH c) s = (if s = [c] then {Char c} else {})"
   and   "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
 unfolding LV_def
 by (auto intro: Prf.intros elim: Prf.cases)
@@ -229,8 +226,8 @@
   case (ONE s)
   show "finite (LV ONE s)" by (simp add: LV_simps)
 next
-  case (CHAR c s)
-  show "finite (LV (CHAR c) s)" by (simp add: LV_simps)
+  case (CH c s)
+  show "finite (LV (CH c) s)" by (simp add: LV_simps)
 next 
   case (ALT r1 r2 s)
   then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
@@ -258,13 +255,13 @@
 
 
 
-section {* Our inductive POSIX Definition *}
+section \<open>Our inductive POSIX Definition\<close>
 
 inductive 
   Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 where
   Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
-| Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
+| Posix_CH: "[c] \<in> (CH c) \<rightarrow> (Char c)"
 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
@@ -278,7 +275,7 @@
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
   "s \<in> ONE \<rightarrow> v"
-  "s \<in> CHAR c \<rightarrow> v"
+  "s \<in> CH c \<rightarrow> v"
   "s \<in> ALT r1 r2 \<rightarrow> v"
   "s \<in> SEQ r1 r2 \<rightarrow> v"
   "s \<in> STAR r \<rightarrow> v"
@@ -287,13 +284,13 @@
   assumes "s \<in> r \<rightarrow> v"
   shows "s \<in> L r" "flat v = s"
 using assms
-by (induct s r v rule: Posix.induct)
-   (auto simp add: Sequ_def)
+  by(induct s r v rule: Posix.induct)
+    (auto simp add: Sequ_def)
 
-text {*
+text \<open>
   For a give value and string, our Posix definition 
   determines a unique value.
-*}
+\<close>
 
 lemma Posix_determ:
   assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
@@ -304,8 +301,8 @@
   have "[] \<in> ONE \<rightarrow> v2" by fact
   then show "Void = v2" by cases auto
 next 
-  case (Posix_CHAR c v2)
-  have "[c] \<in> CHAR c \<rightarrow> v2" by fact
+  case (Posix_CH c v2)
+  have "[c] \<in> CH c \<rightarrow> v2" by fact
   then show "Char c = v2" by cases auto
 next 
   case (Posix_ALT1 s r1 v r2 v2)
@@ -362,9 +359,9 @@
 qed
 
 
-text {*
+text \<open>
   Our POSIX values are lexical values.
-*}
+\<close>
 
 lemma Posix_LV:
   assumes "s \<in> r \<rightarrow> v"