equal
deleted
inserted
replaced
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 rules |
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 |
19 nat_case_def |
19 nat_case_def |
20 "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))" |
20 "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))" |