src/ZF/perm.thy
changeset 124 858ab9a9b047
parent 0 a5a9c433f639
--- a/src/ZF/perm.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/perm.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -9,7 +9,7 @@
   -- Lemmas for the Schroeder-Bernstein Theorem
 *)
 
-Perm = ZF +
+Perm = ZF + "mono" +
 consts
     O    	::      "[i,i]=>i"      (infixr 60)
     id  	::      "i=>i"