src/ZF/Coind/BCR.thy

--- a/src/ZF/Coind/BCR.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/BCR.thy	Mon May 21 14:46:30 2001 +0200
@@ -21,7 +21,7 @@
 defs
   isofenv_def "isofenv(ve,te) ==                
    ve_dom(ve) = te_dom(te) &            
-   ( ALL x:ve_dom(ve).                          
-     EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
+   ( \\<forall>x \\<in> ve_dom(ve).                          
+     \\<exists>c \\<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
   
 end