src/ZF/AC/recfunAC16.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago)
changeset 1401 0c439768f45c
parent 1204 a4253da68be2
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
     1 (*  Title: 	ZF/AC/recfunAC16.thy
     2     ID:         $Id$
     3     Author: 	Krzysztof Grabczewski
     4 
     5 A recursive definition used in the proof of WO2 ==> AC16
     6 *)
     7 
     8 recfunAC16 = Transrec2 + Cardinal +
     9 
    10 consts
    11 
    12   recfunAC16              :: [i, i, i, i] => i
    13 
    14 defs
    15 
    16   recfunAC16_def
    17     "recfunAC16(f,fa,i,a) == 
    18 	 transrec2(i, 0, 
    19 	      %g r. if(EX y:r. fa`g <= y, r, 
    20 		       r Un {f`(LEAST i. fa`g <= f`i & 
    21 		       (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
    22 
    23 end