| changeset 11772 | cf618fe8facd |
| parent 11565 | ab004c0ecc63 |
| child 12742 | 83cd2140977d |
--- a/src/HOL/NanoJava/Example.thy Sun Oct 14 22:15:07 2001 +0200 +++ b/src/HOL/NanoJava/Example.thy Mon Oct 15 17:02:57 2001 +0200 @@ -101,8 +101,8 @@ apply (induct n) by auto -lemma Nat_atleast_reset_locs [rule_format, simp]: - "\<forall>s v. reset_locs s:v \<ge> n = (s:v \<ge> n)" +lemma Nat_atleast_del_locs [rule_format, simp]: + "\<forall>s v. del_locs s:v \<ge> n = (s:v \<ge> n)" apply (induct n) by auto