--- a/thys3/ClosedForms.thy	Mon May 09 17:20:55 2022 +0100
+++ b/thys3/ClosedForms.thy	Mon May 09 17:24:26 2022 +0100
@@ -1547,11 +1547,11 @@
   then have "created_by_star (rder c r2)"
     using "2.hyps"(3) cbs_ders_cbs by auto
   then show ?case
-    
     by (simp add: "2.hyps"(2) "2.hyps"(4))
   qed
 
-
+(*AALTS [a\x . b.c, b\x .c,  c \x]*)
+(*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*)
 
 lemma stupdate_induct1:
   shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =