# HG changeset patch
# User kleing
# Date 979669333 -3600
# Node ID f1209aff9517d5cf3dbc3a655f65371f29d40d1e
# Parent  21ba831562d09d89e07932553bba517486b6873e
Store.thy is obsolete (newref isn't used any more)

diff -r 21ba831562d0 -r f1209aff9517 src/HOL/MicroJava/JVM/JVMState.thy
--- 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 :*}
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