diff -r e4cfa64271ed -r d4b3b0f942f4 thys2/Journal/Paper.thy~
--- a/thys2/Journal/Paper.thy~	Wed Jan 12 15:24:10 2022 +0000
+++ b/thys2/Journal/Paper.thy~	Wed Jan 12 17:08:46 2022 +0000
@@ -50,10 +50,10 @@
   Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and  
 
   ZERO ("\<^bold>0" 81) and 
-  ONE ("\<^bold>1" 81) and 
+  ONE ("\<^bold>1" 81) and                  
   CH ("_" [1000] 80) and
-  ALT ("_ + _" [77,77] 78) and
-  SEQ ("_ \<cdot> _" [77,77] 78) and
+  ALT ("_ + _" [77,77] 77) and
+  SEQ ("_ \<cdot> _" [78,78] 78) and
   STAR ("_\<^sup>\<star>" [79] 78) and
   
   val.Void ("Empty" 78) and
@@ -288,7 +288,7 @@
 
 This rule allows us to simplify \mbox{@{term "(ALT (SEQ (ALT a b) c)  (SEQ a c))"}}
  into  \mbox{@{term "ALT (SEQ a c)  (SEQ b c)"}},
-which is cannot be done under the \mbox{ \<leadsto>} rule because only alternatives which are
+which  cannot be done under the rrewrite rule because only alternatives which are
 children of another alternative can be spilled out.
 \<close>