equal
deleted
inserted
replaced
6 Natural numbers in Zermelo-Fraenkel Set Theory |
6 Natural numbers in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 Nat = Ordinal + Bool + "mono" + |
9 Nat = Ordinal + Bool + "mono" + |
10 consts |
10 consts |
11 nat :: "i" |
11 nat :: i |
12 nat_case :: "[i, i=>i, i]=>i" |
12 nat_case :: [i, i=>i, i]=>i |
13 nat_rec :: "[i, i, [i,i]=>i]=>i" |
13 nat_rec :: [i, i, [i,i]=>i]=>i |
14 |
14 |
15 defs |
15 defs |
16 |
16 |
17 nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})" |
17 nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})" |
18 |
18 |