--- a/src/ZF/Resid/Confluence.thy Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Confluence.thy Mon May 21 14:51:46 2001 +0200
@@ -13,9 +13,9 @@
defs
confluence_def "confluence(R) ==
- ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->
- (EX u.<y,u>:R & <z,u>:R))"
- strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->
- (EX u.(y =1=> u) & (z===>u)))"
+ \\<forall>x y. <x,y>:R --> (\\<forall>z.<x,z>:R -->
+ (\\<exists>u.<y,u>:R & <z,u>:R))"
+ strip_def "strip == \\<forall>x y. (x ===> y) --> (\\<forall>z.(x =1=> z) -->
+ (\\<exists>u.(y =1=> u) & (z===>u)))"
end