--- a/src/ZF/Resid/Confluence.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Confluence.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Confluence.thy
+(* Title: Confluence.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
@@ -8,14 +8,14 @@
Confluence = Reduction+
consts
- confluence :: i=>o
- strip :: o
+ confluence :: i=>o
+ strip :: o
defs
confluence_def "confluence(R) ==
- ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->
- (EX u.<y,u>:R & <z,u>: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)))"
+ (EX u.(y =1=> u) & (z===>u)))"
end