diff -r 21ba831562d0 -r f1209aff9517 src/HOL/MicroJava/JVM/Store.thy
--- a/src/HOL/MicroJava/JVM/Store.thy	Tue Jan 16 19:21:21 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(*  Title:      HOL/MicroJava/JVM/Store.thy
-    ID:         $Id$
-    Author:     Cornelia Pusch
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-header {* Store of the JVM *}
-
-theory Store = Conform:
-
-text {*
-The JVM builds on many notions already defined in Java.
-Conform provides notions for the type safety proof of the Bytecode Verifier.
-*}
-
-
-constdefs
- newref :: "('a \<leadsto> 'b) => 'a"
- "newref s == SOME v. s v = None"
-
-
-lemma newref_None:
-  "hp x = None ==> hp (newref hp) = None"
-by (auto intro: someI2_ex simp add: newref_def)
-
-end