renamed reset_locs to del_locs

--- a/src/HOL/NanoJava/AxSem.thy	Sun Oct 14 22:15:07 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Mon Oct 15 17:02:57 2001 +0200
@@ -79,7 +79,7 @@
 
   Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
     \<forall>a p ls. A |- {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and> 
-                    s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(reset_locs s))}
+                    s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s))}
                   Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
              A |-e {P} {C}e1..m(e2) {S}"
 

--- 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
 

--- a/src/HOL/NanoJava/OpSem.thy	Sun Oct 14 22:15:07 2001 +0200
+++ b/src/HOL/NanoJava/OpSem.thy	Mon Oct 15 17:02:57 2001 +0200
@@ -54,7 +54,7 @@
             s -Cast C e>v-n-> s'"
 
   Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; 
-            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(reset_locs s2)) -Meth (C,m)-n-> s3
+            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n-> s3
      |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
 
   Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;

--- a/src/HOL/NanoJava/State.thy	Sun Oct 14 22:15:07 2001 +0200
+++ b/src/HOL/NanoJava/State.thy	Mon Oct 15 17:02:57 2001 +0200
@@ -52,8 +52,8 @@
 
 constdefs
 
-  reset_locs     :: "state => state"
- "reset_locs s \<equiv> s (| locals := empty |)"
+  del_locs     :: "state => state"
+ "del_locs s \<equiv> s (| locals := empty |)"
 
   init_locs     :: "cname => mname => state => state"
  "init_locs C m s \<equiv> s (| locals := locals s ++ 
@@ -122,8 +122,8 @@
 by (simp add: lupd_def get_field_def set_locs_def get_obj_def)
 
 lemma get_field_set_locs [simp]:
-  "get_field (reset_locs s) a f = get_field s a f"
-by (simp add: lupd_def get_field_def reset_locs_def get_obj_def)
+  "get_field (del_locs s) a f = get_field s a f"
+by (simp add: lupd_def get_field_def del_locs_def get_obj_def)
 
 lemma new_obj_get_local [simp]: "new_obj a C s <x> = s<x>"
 by (simp add: new_obj_def hupd_def get_local_def)
@@ -141,8 +141,8 @@
 lemma hupd_hupd [simp]: "hupd(a\<mapsto>obj) (hupd(a\<mapsto>obj') s) = hupd(a\<mapsto>obj) s"
 by (simp add: hupd_def)
 
-lemma heap_reset_locs [simp]: "heap (reset_locs s) = heap s"
-by (simp add: reset_locs_def)
+lemma heap_del_locs [simp]: "heap (del_locs s) = heap s"
+by (simp add: del_locs_def)
 
 lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s"
 by (simp add: set_locs_def)
@@ -151,24 +151,24 @@
   "hupd(a\<mapsto>obj) (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (hupd(a\<mapsto>obj) s)"
 by (simp add: hupd_def lupd_def)
 
-lemma hupd_reset_locs [simp]: 
-  "hupd(a\<mapsto>obj) (reset_locs s) = reset_locs (hupd(a\<mapsto>obj) s)"
-by (simp add: hupd_def reset_locs_def)
+lemma hupd_del_locs [simp]: 
+  "hupd(a\<mapsto>obj) (del_locs s) = del_locs (hupd(a\<mapsto>obj) s)"
+by (simp add: hupd_def del_locs_def)
 
 lemma new_obj_lupd [simp]: 
   "new_obj a C (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (new_obj a C s)"
 by (simp add: new_obj_def)
 
-lemma new_obj_reset_locs [simp]: 
-  "new_obj a C (reset_locs s) = reset_locs (new_obj a C s)"
+lemma new_obj_del_locs [simp]: 
+  "new_obj a C (del_locs s) = del_locs (new_obj a C s)"
 by (simp add: new_obj_def)
 
 lemma upd_obj_lupd [simp]: 
   "upd_obj a f v (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (upd_obj a f v s)"
 by (simp add: upd_obj_def Let_def split_beta)
 
-lemma upd_obj_reset_locs [simp]: 
-  "upd_obj a f v (reset_locs s) = reset_locs (upd_obj a f v s)"
+lemma upd_obj_del_locs [simp]: 
+  "upd_obj a f v (del_locs s) = del_locs (upd_obj a f v s)"
 by (simp add: upd_obj_def Let_def split_beta)
 
 lemma get_field_hupd_same [simp]: