diff -r 0c491eff5b01 -r 14e5ae1fb541 progs/Matcher.thy --- a/progs/Matcher.thy Mon Feb 03 13:25:59 2025 +0000 +++ b/progs/Matcher.thy Fri Sep 05 16:59:48 2025 +0100 @@ -107,6 +107,8 @@ apply(simp only: L.simps) apply(simp) (* SEQ case *) +apply(simp only: L.simps) +apply(simp) oops lemma nullable_correctness: