diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Language.thy	Mon May 21 14:46:30 2001 +0200
@@ -11,8 +11,8 @@
   c_app :: [i,i] => i           (*Abstract constructor for fun application*)
 
 rules
-  constNEE  "c:Const ==> c ~= 0"
-  c_appI    "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const"
+  constNEE  "c \\<in> Const ==> c \\<noteq> 0"
+  c_appI    "[| c1 \\<in> Const; c2 \\<in> Const |] ==> c_app(c1,c2):Const"
 
 
 consts
@@ -20,10 +20,10 @@
   ExVar :: i                    (* Abstract type of variables *)
 
 datatype
-  "Exp" = e_const ("c:Const")
-        | e_var ("x:ExVar")
-        | e_fn ("x:ExVar","e:Exp")
-        | e_fix ("x1:ExVar","x2:ExVar","e:Exp")
-        | e_app ("e1:Exp","e2:Exp")
+  "Exp" = e_const ("c \\<in> Const")
+        | e_var ("x \\<in> ExVar")
+        | e_fn ("x \\<in> ExVar","e \\<in> Exp")
+        | e_fix ("x1 \\<in> ExVar","x2 \\<in> ExVar","e \\<in> Exp")
+        | e_app ("e1 \\<in> Exp","e2 \\<in> Exp")
 
 end