src/HOL/MicroJava/J/Value.thy
changeset 10042 7164dc0d24d8
parent 9346 297dcbf64526
child 10061 fe82134773dc
     1.1 --- a/src/HOL/MicroJava/J/Value.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Value.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -22,9 +22,9 @@
     1.4  translations "val" <= (type) "val_"
     1.5  
     1.6  consts
     1.7 -  the_Bool	:: "val \\<Rightarrow> bool"
     1.8 -  the_Intg	:: "val \\<Rightarrow> int"
     1.9 -  the_Addr	:: "val \\<Rightarrow> loc"
    1.10 +  the_Bool	:: "val => bool"
    1.11 +  the_Intg	:: "val => int"
    1.12 +  the_Addr	:: "val => loc"
    1.13  
    1.14  primrec
    1.15   "the_Bool (Bool b) = b"
    1.16 @@ -36,8 +36,8 @@
    1.17   "the_Addr (Addr a) = a"
    1.18  
    1.19  consts
    1.20 -  defpval	:: "prim_ty \\<Rightarrow> val"	(* default value for primitive types *)
    1.21 -  default_val	:: "ty \\<Rightarrow> val"		(* default value for all types *)
    1.22 +  defpval	:: "prim_ty => val"	(* default value for primitive types *)
    1.23 +  default_val	:: "ty => val"		(* default value for all types *)
    1.24  
    1.25  primrec
    1.26  	"defpval Void    = Unit"