thys3/ClosedForms.thy
changeset 543 b2bea5968b89
parent 513 ca7ca1f10f98
child 554 15d182ffbc76
--- a/thys3/ClosedForms.thy	Tue Jun 14 18:06:33 2022 +0100
+++ b/thys3/ClosedForms.thy	Thu Jun 23 16:09:40 2022 +0100
@@ -1491,7 +1491,8 @@
 lemma seq_closed_form_variant: 
   assumes "s \<noteq> []"
   shows "rders_simp (RSEQ r1 r2) s = 
-             rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # (map (rders_simp r2) (vsuf s r1))))"
+             rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # 
+        (map (rders_simp r2) (vsuf s r1))))"
   using assms q seq_closed_form by force