author | clasohm |
Thu, 22 Jun 1995 17:13:05 +0200 | |
changeset 1155 | 928a16e02f9f |
parent 1123 | 5dfdc1464966 |
child 1196 | d43c1f7a53fe |
permissions | -rw-r--r-- |
(* Title: ZF/AC/HH.thy ID: $Id$ Author: Krzysztof Gr`abczewski The theory file for the proofs of AC17 ==> AC1 AC1 ==> WO2 AC15 ==> WO6 *) HH = AC_Equiv + Hartog + WO_AC + consts HH :: "[i, i, i] => i" defs HH_def "HH(f,x,a) == transrec(a, %b r. (lam z:Pow(x). if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))" end