--- a/src/HOL/MicroJava/J/Value.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Fri Sep 22 16:28:53 2000 +0200
@@ -8,44 +8,45 @@
Value = Type +
-types loc (* locations, i.e. abstract references on objects *)
+types loc (* locations, i.e. abstract references on objects *)
arities loc :: term
-datatype val_ (* name non 'val' because of clash with ML token *)
- = Unit (* dummy result value of void methods *)
- | Null (* null reference *)
- | Bool bool (* Boolean value *)
- | Intg int (* integer value *) (* Name Intg instead of Int because
- of clash with HOL/Set.thy *)
- | Addr loc (* addresses, i.e. locations of objects *)
+datatype val_ (* name non 'val' because of clash with ML token *)
+ = Unit (* dummy result value of void methods *)
+ | Null (* null reference *)
+ | Bool bool (* Boolean value *)
+ | Intg int (* integer value, name Intg instead of Int because
+ of clash with HOL/Set.thy *)
+ | Addr loc (* addresses, i.e. locations of objects *)
+
types val = val_
translations "val" <= (type) "val_"
consts
- the_Bool :: "val => bool"
- the_Intg :: "val => int"
- the_Addr :: "val => loc"
+ the_Bool :: "val => bool"
+ the_Intg :: "val => int"
+ the_Addr :: "val => loc"
primrec
- "the_Bool (Bool b) = b"
+ "the_Bool (Bool b) = b"
primrec
- "the_Intg (Intg i) = i"
+ "the_Intg (Intg i) = i"
primrec
- "the_Addr (Addr a) = a"
+ "the_Addr (Addr a) = a"
consts
- defpval :: "prim_ty => val" (* default value for primitive types *)
- default_val :: "ty => val" (* default value for all types *)
+ defpval :: "prim_ty => val" (* default value for primitive types *)
+ default_val :: "ty => val" (* default value for all types *)
primrec
- "defpval Void = Unit"
- "defpval Boolean = Bool False"
- "defpval Integer = Intg (#0)"
+ "defpval Void = Unit"
+ "defpval Boolean = Bool False"
+ "defpval Integer = Intg (#0)"
primrec
- "default_val (PrimT pt) = defpval pt"
- "default_val (RefT r ) = Null"
+ "default_val (PrimT pt) = defpval pt"
+ "default_val (RefT r ) = Null"
end