src/ZF/AC.thy
changeset 6053 8a1059aa01f0
parent 2469 b50b8c0eec01
child 13134 bf37a3049251
     1.1 --- a/src/ZF/AC.thy	Mon Dec 28 16:58:11 1998 +0100
     1.2 +++ b/src/ZF/AC.thy	Mon Dec 28 16:59:28 1998 +0100
     1.3 @@ -9,6 +9,12 @@
     1.4  *)
     1.5  
     1.6  AC = func +
     1.7 +
     1.8 +constdefs
     1.9 +  (*Needs to be visible for Zorn.thy*)
    1.10 +  increasing :: i=>i
    1.11 +    "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
    1.12 +
    1.13  rules
    1.14    AC    "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
    1.15  end