diff -r a7344c9afbaf -r b2bea5968b89 thys3/ClosedForms.thy --- 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 \ []" 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