--- a/src/ZF/Perm.thy Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Perm.thy Thu Aug 10 11:27:34 2000 +0200
@@ -9,7 +9,7 @@
-- Lemmas for the Schroeder-Bernstein Theorem
*)
-Perm = upair + mono + func +
+Perm = mono + func +
consts
O :: [i,i]=>i (infixr 60)