diff -r aa0a2a3f90a0 -r f5866f1d6a59 thys2/Journal/Paper.thy
--- a/thys2/Journal/Paper.thy	Fri Jan 07 22:29:14 2022 +0000
+++ b/thys2/Journal/Paper.thy	Sat Jan 08 15:26:33 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
@@ -286,8 +286,10 @@
   \end{tabular}
 \end{center}
 
-This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}}
-
+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  cannot be done under the rrewrite rule because only alternatives which are
+children of another alternative can be spilled out.
 \<close>
 
 (*This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}}