equal
deleted
inserted
replaced
20 |
20 |
21 primrec "op -" nat |
21 primrec "op -" nat |
22 diff_0 "m - 0 = m" |
22 diff_0 "m - 0 = m" |
23 diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)" |
23 diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)" |
24 |
24 |
25 syntax pred :: nat => nat |
|
26 translations "pred m" => "m - 1" |
|
27 |
|
28 primrec "op *" nat |
25 primrec "op *" nat |
29 mult_0 "0 * n = 0" |
26 mult_0 "0 * n = 0" |
30 mult_Suc "Suc m * n = n + (m * n)" |
27 mult_Suc "Suc m * n = n + (m * n)" |
31 |
28 |
32 end |
29 end |