author | clasohm |
Tue, 06 Feb 1996 12:27:17 +0100 | |
changeset 1478 | 2b8c2a7547ab |
parent 1401 | 0c439768f45c |
child 2469 | b50b8c0eec01 |
permissions | -rw-r--r-- |
(* Title: ZF/AC/recfunAC16.thy ID: $Id$ Author: Krzysztof Grabczewski A recursive definition used in the proof of WO2 ==> AC16 *) recfunAC16 = Transrec2 + Cardinal + consts recfunAC16 :: [i, i, i, i] => i defs recfunAC16_def "recfunAC16(f,fa,i,a) == transrec2(i, 0, %g r. if(EX y:r. fa`g <= y, r, r Un {f`(LEAST i. fa`g <= f`i & (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))" end