diff -r 664322da08fe -r ee53acaf2420 thys2/Journal/Paper.thy
--- a/thys2/Journal/Paper.thy	Thu Nov 04 13:52:17 2021 +0000
+++ b/thys2/Journal/Paper.thy	Tue Dec 14 16:06:42 2021 +0000
@@ -265,10 +265,34 @@
 @{thm blexersimp_correctness}
 \end{lemma}
 
-The nice thing about the aove
+The nice thing about the above
 \<close>
 
 
+section \<open> Additional Simp Rules?\<close>
+
+
+text  \<open>
+One question someone would ask is:
+can we add more "atomic" simplification/rewriting rules,
+so the simplification is even more aggressive, making
+the intermediate results smaller, and therefore more space-efficient? 
+For example, one might want to do open up alternatives who is a child
+of a sequence:
+
+\begin{center}
+  \begin{tabular}{lcl}
+    @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]}\\
+  \end{tabular}
+\end{center}
+
+
+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>
+
 
 section \<open>Introduction\<close>
 
@@ -2055,9 +2079,19 @@
 end
 (*>*)
 
+
+
 (*
 
 \begin{center}
+  \begin{tabular}
+    @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]}
+  end{tabular}
+\end{center}
+
+
+
+\begin{center}
   \begin{tabular}{lcl}
   @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\
   @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\