lemma now in Store.thy
authorkleing
Fri Sep 22 13:13:15 2000 +0200 (2000-09-22)
changeset 100587b2be4d2703a
parent 10057 8c8d2d0d3ef8
child 10059 f56da4769355
lemma now in Store.thy
src/HOL/MicroJava/JVM/Store.ML
     1.1 --- a/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 22 13:12:19 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,10 +0,0 @@
     1.4 -(*  Title:      HOL/MicroJava/JVM/Store.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Cornelia Pusch
     1.7 -    Copyright   1999 Technische Universitaet Muenchen
     1.8 -*)
     1.9 -
    1.10 -Goalw [newref_def]
    1.11 - "hp x = None --> hp (newref hp) = None";
    1.12 -by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1);
    1.13 -qed_spec_mp "newref_None";