--- a/src/ZF/Perm.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Perm.thy Tue Nov 29 00:31:31 1994 +0100
@@ -15,7 +15,7 @@
id :: "i=>i"
inj,surj,bij:: "[i,i]=>i"
-rules
+defs
(*composition of relations and functions; NOT Suppes's relative product*)
comp_def "r O s == {xz : domain(s)*range(r) . \