diff -r 8bb064045b4e -r e51c9a67a68d thys/Exercises.thy
--- a/thys/Exercises.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Exercises.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -9,7 +9,7 @@
 where
   "zeroable (ZERO) \<longleftrightarrow> True"
 | "zeroable (ONE) \<longleftrightarrow> False"
-| "zeroable (CHAR c) \<longleftrightarrow> False"
+| "zeroable (CH c) \<longleftrightarrow> False"
 | "zeroable (ALT r1 r2) \<longleftrightarrow> zeroable r1 \<and> zeroable r2"
 | "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2"
 | "zeroable (STAR r) \<longleftrightarrow> False"
@@ -24,7 +24,7 @@
 where
   "atmostempty (ZERO) \<longleftrightarrow> True"
 | "atmostempty (ONE) \<longleftrightarrow> True"
-| "atmostempty (CHAR c) \<longleftrightarrow> False"
+| "atmostempty (CH c) \<longleftrightarrow> False"
 | "atmostempty (ALT r1 r2) \<longleftrightarrow> atmostempty r1 \<and> atmostempty r2"
 | "atmostempty (SEQ r1 r2) \<longleftrightarrow> 
      zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)"
@@ -37,7 +37,7 @@
 where
   "somechars (ZERO) \<longleftrightarrow> False"
 | "somechars (ONE) \<longleftrightarrow> False"
-| "somechars (CHAR c) \<longleftrightarrow> True"
+| "somechars (CH c) \<longleftrightarrow> True"
 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2"
 | "somechars (SEQ r1 r2) \<longleftrightarrow> 
       (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> 
@@ -69,7 +69,7 @@
 where
   "leastsinglechar (ZERO) \<longleftrightarrow> False"
 | "leastsinglechar (ONE) \<longleftrightarrow> False"
-| "leastsinglechar (CHAR c) \<longleftrightarrow> True"
+| "leastsinglechar (CH c) \<longleftrightarrow> True"
 | "leastsinglechar (ALT r1 r2) \<longleftrightarrow> leastsinglechar r1 \<or> leastsinglechar r2"
 | "leastsinglechar (SEQ r1 r2) \<longleftrightarrow> 
       (if (zeroable r1 \<or> zeroable r2) then False
@@ -96,7 +96,7 @@
 where
   "infinitestrings (ZERO) = False"
 | "infinitestrings (ONE) = False"
-| "infinitestrings (CHAR c) = False"
+| "infinitestrings (CH c) = False"
 | "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)"
 | "infinitestrings (SEQ r1 r2) \<longleftrightarrow> 
       (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)"