changeset 436 | 222333d2bdc2 |
parent 425 | 14c558ae0b09 |
--- a/thys2/SizeBound4.thy Mon Feb 21 23:38:26 2022 +0000 +++ b/thys2/SizeBound4.thy Wed Mar 02 11:43:41 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)