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
@@ -217,11 +217,6 @@
   @{thm[mode=Rule] rrewrite.intros(6)[of "r" "r'" "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\
   @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "rs\<^sub>a" "rs\<^sub>b"]}\\
   @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "rs\<^sub>a" "bs\<^sub>1" "rs\<^sub>1" "rs\<^sub>b"]}\\
-  @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\
-  @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\
-  @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" "r\<^sub>1"]}\\
-  @{thm[mode=Rule] rrewrite.intros(12)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\
-
   \end{tabular}
 \end{center}
 
@@ -268,7 +263,11 @@
 The nice thing about the above
 \<close>
 
-
+(*  @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\
+  @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\
+  @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" "r\<^sub>1"]}\\
+  @{thm[mode=Rule] rrewrite.intros(12)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\
+*)
 section \<open> Additional Simp Rules?\<close>
 
 
@@ -290,6 +289,12 @@
  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.
+
+Now with this rule we have some examples where we get
+even smaller intermediate derivatives than not having this
+rule:
+$\textit{(a+aa)}^* \rightarrow \textit{(1+1a)(a+aa)}^* \rightarrow
+ \textit{(1+a)(a+aa)}^* $
 \<close>
 
 (*This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}}