changeset 439 | a5376206fd52 |
parent 436 | 222333d2bdc2 |
--- a/thys2/SizeBound4.thy Wed Mar 02 23:13:59 2022 +0000 +++ b/thys2/SizeBound4.thy Wed Mar 02 23:23:19 2022 +0000 @@ -1019,7 +1019,7 @@ apply(simp only: map_append) apply(simp only: map_single) apply(rule rs_in_rstar) - thm rrewrite_srewrite.intros + thm rrewrite_srewrite.intros apply(rule rrewrite_srewrite.ss6) using as apply(auto simp add: der_correctness Der_def)