src/HOL/NanoJava/State.thy
changeset 13524 604d0f3622d6
parent 11772 cf618fe8facd
child 14134 0fdf5708c7a8
     1.1 --- a/src/HOL/NanoJava/State.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/NanoJava/State.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4    "get_field (set_locs l s) a f = get_field s a f"
     1.5  by (simp add: lupd_def get_field_def set_locs_def get_obj_def)
     1.6  
     1.7 -lemma get_field_set_locs [simp]:
     1.8 +lemma get_field_del_locs [simp]:
     1.9    "get_field (del_locs s) a f = get_field s a f"
    1.10  by (simp add: lupd_def get_field_def del_locs_def get_obj_def)
    1.11