src/HOL/MicroJava/JVM/Store.thy

--- a/src/HOL/MicroJava/JVM/Store.thy	Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.thy	Fri Sep 22 13:12:19 2000 +0200
@@ -2,17 +2,25 @@
     ID:         $Id$
     Author:     Cornelia Pusch
     Copyright   1999 Technische Universitaet Muenchen
-
-The store.
-
-The JVM builds on many notions already defined in Java.
-Conform provides notions for the type safety proof of the Bytecode Verifier.
 *)
 
-Store = Conform +  
+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 :: "('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