author | paulson |
Thu, 10 Sep 1998 17:42:44 +0200 | |
changeset 5470 | 855654b691db |
parent 1478 | 2b8c2a7547ab |
child 11317 | 7f9e4c389318 |
permissions | -rw-r--r-- |
(* Title: ZF/AC/HH.thy ID: $Id$ Author: Krzysztof Grabczewski The theory file for the proofs of AC17 ==> AC1 AC1 ==> WO2 AC15 ==> WO6 *) HH = AC_Equiv + Hartog + WO_AC + Let + consts HH :: [i, i, i] => i defs HH_def "HH(f,x,a) == transrec(a, %b r. let z = x - (UN c:b. r`c) in if(f`z:Pow(z)-{0}, f`z, {x}))" end