--- a/thys3/ClosedForms.thy	Wed Jun 29 12:38:05 2022 +0100
+++ b/thys3/ClosedForms.thy	Fri Jul 01 13:02:15 2022 +0100
@@ -887,14 +887,16 @@
   using rders_simp_same_simpders rsimp_idem by auto
 
 lemma repeated_altssimp:
-  shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =
+  shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> 
+           rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =
            rsimp_ALTs (rdistinct (rflts rs) {})"
   by (metis map_idI rsimp.simps(2) rsimp_idem)
 
 
 
 lemma alts_closed_form: 
-  shows "rsimp (rders_simp (RALTS rs) s) = rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
+  shows "rsimp (rders_simp (RALTS rs) s) = 
+         rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
   apply(induct s rule: rev_induct)
    apply simp
   apply simp