--- a/src/HOL/MicroJava/J/Value.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Thu Sep 21 10:42:49 2000 +0200
@@ -22,9 +22,9 @@
translations "val" <= (type) "val_"
consts
- the_Bool :: "val \\<Rightarrow> bool"
- the_Intg :: "val \\<Rightarrow> int"
- the_Addr :: "val \\<Rightarrow> loc"
+ the_Bool :: "val => bool"
+ the_Intg :: "val => int"
+ the_Addr :: "val => loc"
primrec
"the_Bool (Bool b) = b"
@@ -36,8 +36,8 @@
"the_Addr (Addr a) = a"
consts
- defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *)
- default_val :: "ty \\<Rightarrow> 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"