equal
deleted
inserted
replaced
7 |
7 |
8 |
8 |
9 PNat = Main + |
9 PNat = Main + |
10 |
10 |
11 typedef |
11 typedef |
12 pnat = "lfp(%X. {1} Un Suc`X)" (lfp_def) |
12 pnat = "lfp(%X. {1'} Un Suc`X)" (lfp_def) |
13 |
13 |
14 instance |
14 instance |
15 pnat :: {ord, plus, times} |
15 pnat :: {ord, plus, times} |
16 |
16 |
17 consts |
17 consts |
25 "pnat_of_nat n == Abs_pnat(n + 1)" |
25 "pnat_of_nat n == Abs_pnat(n + 1)" |
26 |
26 |
27 defs |
27 defs |
28 |
28 |
29 pnat_one_def |
29 pnat_one_def |
30 "1p == Abs_pnat(1)" |
30 "1p == Abs_pnat(1')" |
31 pnat_Suc_def |
31 pnat_Suc_def |
32 "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))" |
32 "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))" |
33 |
33 |
34 pnat_add_def |
34 pnat_add_def |
35 "x + y == Abs_pnat(Rep_pnat(x) + Rep_pnat(y))" |
35 "x + y == Abs_pnat(Rep_pnat(x) + Rep_pnat(y))" |