equal
deleted
inserted
replaced
5 |
5 |
6 AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux + |
6 AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux + |
7 |
7 |
8 consts |
8 consts |
9 |
9 |
10 ww :: "[i, i] => i" |
10 ww :: [i, i] => i |
11 s_u :: "[i, i, i, i] => i" |
11 s_u :: [i, i, i, i] => i |
12 MM :: "[i, i, i] => i" |
12 MM :: [i, i, i] => i |
13 LL :: "[i, i, i] => i" |
13 LL :: [i, i, i] => i |
14 GG :: "[i, i, i] => i" |
14 GG :: [i, i, i] => i |
15 |
15 |
16 defs |
16 defs |
17 |
17 |
18 ww_def "ww(x, k) == {u:Pow(x). u eqpoll k}" |
18 ww_def "ww(x, k) == {u:Pow(x). u eqpoll k}" |
19 |
19 |