lemma now in Store.thy

--- a/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 22 13:12:19 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-(*  Title:      HOL/MicroJava/JVM/Store.thy
-    ID:         $Id$
-    Author:     Cornelia Pusch
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-Goalw [newref_def]
- "hp x = None --> hp (newref hp) = None";
-by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1);
-qed_spec_mp "newref_None";