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