--- a/src/ZF/Resid/Confluence.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Confluence.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
Confluence = Reduction+
consts
- confluence :: "i=>o"
- strip :: "o"
+ confluence :: i=>o
+ strip :: o
defs
confluence_def "confluence(R) ==