src/HOL/MicroJava/J/Type.thy
changeset 10042 7164dc0d24d8
parent 8032 1eaae1a2f8ff
child 10061 fe82134773dc
     1.1 --- a/src/HOL/MicroJava/J/Type.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Type.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  syntax
     1.6           NT     :: "          ty"
     1.7 -	 Class	:: "cname  \\<Rightarrow> ty"
     1.8 +	 Class	:: "cname  => ty"
     1.9  translations
    1.10  	"NT"      == "RefT   NullT"
    1.11  	"Class C" == "RefT (ClassT C)"