# HG changeset patch
# User Chengsong
# Date 1652113466 -3600
# Node ID ca7ca1f10f98c3205a6b436ffa5be48936ee8078
# Parent  a4b86ced5c323dad314f74fbd2cd7e95428a24be
more isarfy

diff -r a4b86ced5c32 -r ca7ca1f10f98 thys3/ClosedForms.thy
--- 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) =