diff -r 22dce9134953 -r a0b16d42d489 src/HOL/Bali/Value.thy
--- 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)"