Store.thy is obsolete (newref isn't used any more)

--- a/src/HOL/MicroJava/JVM/JVMState.thy	Tue Jan 16 19:21:21 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Tue Jan 16 19:22:13 2001 +0100
@@ -8,7 +8,7 @@
 header {* State of the JVM *}
 
 
-theory JVMState = Store:
+theory JVMState = Conform:
 
 
 text {* frame stack :*}

--- 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