src/HOL/MicroJava/JVM/Store.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/Store.thy	Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,23 @@
+(*  Title:      HOL/MicroJava/JVM/Store.thy
+    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 +  
+
+syntax
+ value	:: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b"			("_ \\<And> _")		
+translations
+ "t \\<And> x"  == "the (t x)"
+
+constdefs
+ newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
+ "newref s \\<equiv> \\<epsilon>v. s v = None"
+
+end