diff -r 28458dec90f8 -r c892847df987 thys2/Journal/Paper.thy
--- a/thys2/Journal/Paper.thy	Tue Dec 14 16:17:45 2021 +0000
+++ b/thys2/Journal/Paper.thy	Tue Dec 14 16:32:33 2021 +0000
@@ -286,14 +286,14 @@
   \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)"}}
+\<close>
+
+(*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  \<leadsto> rule because only alternatives which are 
-children of another alternative can be spilled out.
-\<close>
-
-
+children of another alternative can be spilled out.*)
 section \<open>Introduction\<close>