--- a/src/HOL/MicroJava/J/State.thy Mon May 15 17:32:39 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy Mon May 15 17:34:05 2000 +0200
@@ -8,23 +8,24 @@
State = WellType +
-constdefs
-
+consts
the_Bool :: "val \\<Rightarrow> bool"
- "the_Bool v \\<equiv> \\<epsilon>b. v = Bool b"
-
the_Int :: "val \\<Rightarrow> int"
- "the_Int v \\<equiv> \\<epsilon>i. v = Intg i"
-
the_Addr :: "val \\<Rightarrow> loc"
- "the_Addr v \\<equiv> \\<epsilon>a. v = Addr a"
-
-consts
defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *)
default_val :: "ty \\<Rightarrow> val" (* default value for all types *)
primrec
+ "the_Bool (Bool b) = b"
+
+primrec
+ "the_Int (Intg i) = i"
+
+primrec
+ "the_Addr (Addr a) = a"
+
+primrec
"defpval Void = Unit"
"defpval Boolean = Bool False"
"defpval Integer = Intg (#0)"