diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Dynamic.thy
--- a/src/ZF/Coind/Dynamic.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Dynamic.thy	Mon May 21 14:46:30 2001 +0200
@@ -12,25 +12,25 @@
   domains "EvalRel" <= "ValEnv * Exp * Val"
   intrs
     eval_constI
-      " [| ve:ValEnv; c:Const |] ==>   
+      " [| ve \\<in> ValEnv; c \\<in> Const |] ==>   
        <ve,e_const(c),v_const(c)>:EvalRel"
     eval_varI
-      " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>   
+      " [| ve \\<in> ValEnv; x \\<in> ExVar; x \\<in> ve_dom(ve) |] ==>   
        <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
     eval_fnI
-      " [| ve:ValEnv; x:ExVar; e:Exp |] ==>   
+      " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp |] ==>   
        <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
     eval_fixI
-      " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;   
+      " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val;   
           v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   
        <ve,e_fix(f,x,e),cl>:EvalRel " 
     eval_appI1
-      " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   
+      " [| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const;   
           <ve,e1,v_const(c1)>:EvalRel;   
           <ve,e2,v_const(c2)>:EvalRel |] ==>   
        <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
     eval_appI2
-      " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;   
+      " [| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val;   
           <ve,e1,v_clos(xm,em,vem)>:EvalRel;   
           <ve,e2,v2>:EvalRel;   
           <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>