# HG changeset patch
# User kleing
# Date 969621195 -7200
# Node ID 7b2be4d2703a74d22e8d45d5524b28fa20f6f703
# Parent  8c8d2d0d3ef8a87451f4b99bf5ab10079a2d1ae0
lemma now in Store.thy

diff -r 8c8d2d0d3ef8 -r 7b2be4d2703a src/HOL/MicroJava/JVM/Store.ML
--- 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";