diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/ECR.thy
--- a/src/ZF/Coind/ECR.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/ECR.thy	Mon May 21 14:46:30 2001 +0200
@@ -14,12 +14,12 @@
   domains "HasTyRel" <= "Val * Ty"
   intrs
     htr_constI
-      "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
+      "[| c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
     htr_closI
-      "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; 
+      "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv; 
           <te,e_fn(x,e),t>:ElabRel;  
           ve_dom(ve) = te_dom(te);   
-          {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
+          {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}:Pow(HasTyRel)  
       |] ==>   
       <v_clos(x,e,ve),t>:HasTyRel" 
   monos  Pow_mono
@@ -33,6 +33,6 @@
   hastyenv_def 
     " hastyenv(ve,te) ==                        
      ve_dom(ve) = te_dom(te) &          
-     (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+     (\\<forall>x \\<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
 
 end