--- a/src/HOL/MicroJava/J/Type.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Thu Sep 21 10:42:49 2000 +0200
@@ -31,7 +31,7 @@
syntax
NT :: " ty"
- Class :: "cname \\<Rightarrow> ty"
+ Class :: "cname => ty"
translations
"NT" == "RefT NullT"
"Class C" == "RefT (ClassT C)"