| changeset 3235 | 351565b7321b |
| parent 2887 | 00b8ee790d89 |
| child 3308 | da002cef7090 |
| 3234:503f4c8c29eb | 3235:351565b7321b |
|---|---|
26 primrec "op +" nat |
26 primrec "op +" nat |
27 "0 + n = n" |
27 "0 + n = n" |
28 "Suc m + n = Suc(m + n)" |
28 "Suc m + n = Suc(m + n)" |
29 |
29 |
30 primrec "op -" nat |
30 primrec "op -" nat |
31 "m - 0 = m" |
31 diff_0 "m - 0 = m" |
32 "m - Suc n = pred(m - n)" |
32 diff_Suc "m - Suc n = pred(m - n)" |
33 |
33 |
34 primrec "op *" nat |
34 primrec "op *" nat |
35 "0 * n = 0" |
35 "0 * n = 0" |
36 "Suc m * n = n + (m * n)" |
36 "Suc m * n = n + (m * n)" |
37 |
37 |