src/ZF/AC/AC16_WO4.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago)
changeset 1401 0c439768f45c
parent 1203 a39bec971684
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
     1 (*  Title: 	ZF/AC/AC16_WO4.thy
     2     ID:         $Id$
     3     Author: 	Krzysztof Grabczewski
     4 *)
     5 
     6 AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
     7 
     8 consts
     9 
    10   ww  :: [i, i] => i
    11   s_u :: [i, i, i, i] => i
    12   MM  :: [i, i, i] => i
    13   LL  :: [i, i, i] => i
    14   GG  :: [i, i, i] => i
    15   
    16 defs
    17 
    18   ww_def  "ww(x, k) == {u:Pow(x). u eqpoll k}"
    19 
    20   s_u_def "s_u(u, t_n, k, y) == {v:t_n. u:v & k lepoll v Int y}"
    21 
    22   MM_def  "MM(t_n, k, y) == {v:t_n. k lepoll v Int y}"
    23 
    24   LL_def  "LL(t_n, k, y) == {v Int y. v:MM(t_n, k, y)}"
    25 
    26   GG_def  "GG(t_n, k, y) == lam v:LL(t_n, k, y). 
    27 	                    (THE w. w:MM(t_n, k, y) & v <= w) - v"
    28 
    29 end