diff -r b7b100a2de1d -r cf618fe8facd src/HOL/NanoJava/Example.thy
--- 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