src/ZF/AC.thy

--- a/src/ZF/AC.thy	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/AC.thy	Mon Dec 28 16:59:28 1998 +0100
@@ -9,6 +9,12 @@
 *)
 
 AC = func +
+
+constdefs
+  (*Needs to be visible for Zorn.thy*)
+  increasing :: i=>i
+    "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
+
 rules
   AC    "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
 end