--- a/src/HOL/Bali/Value.thy Wed Oct 30 12:44:18 2002 +0100
+++ b/src/HOL/Bali/Value.thy Thu Oct 31 18:27:10 2002 +0100
@@ -9,15 +9,15 @@
theory Value = Type:
-typedecl loc (* locations, i.e. abstract references on objects *)
+typedecl loc --{* locations, i.e. abstract references on objects *}
arities loc :: "type"
datatype val
- = Unit (* dummy result value of void methods *)
- | Bool bool (* Boolean value *)
- | Intg int (* integer value *)
- | Null (* null reference *)
- | Addr loc (* addresses, i.e. locations of objects *)
+ = Unit --{* dummy result value of void methods *}
+ | Bool bool --{* Boolean value *}
+ | Intg int --{* integer value *}
+ | Null --{* null reference *}
+ | Addr loc --{* addresses, i.e. locations of objects *}
translations "val" <= (type) "Term.val"
@@ -33,8 +33,8 @@
types dyn_ty = "loc \<Rightarrow> ty option"
consts
typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
- defpval :: "prim_ty \<Rightarrow> val" (* default value for primitive types *)
- default_val :: " ty \<Rightarrow> val" (* default value for all types *)
+ defpval :: "prim_ty \<Rightarrow> val" --{* default value for primitive types *}
+ default_val :: " ty \<Rightarrow> val" --{* default value for all types *}
primrec "typeof dt Unit = Some (PrimT Void)"
"typeof dt (Bool b) = Some (PrimT Boolean)"