--- a/src/ZF/Perm.thy Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/Perm.thy Fri Jan 03 15:01:55 1997 +0100
@@ -9,7 +9,7 @@
-- Lemmas for the Schroeder-Bernstein Theorem
*)
-Perm = ZF + "mono" +
+Perm = upair + mono + func +
consts
O :: [i,i]=>i (infixr 60)