equal
deleted
inserted
replaced
10 |
10 |
11 types nat |
11 types nat |
12 arities nat :: term |
12 arities nat :: term |
13 |
13 |
14 consts |
14 consts |
15 succ,pred :: "nat => nat" |
15 succ,pred :: nat => nat |
16 "0" :: "nat" ("0") |
16 "0" :: nat ("0") |
17 "+" :: "[nat,nat] => nat" (infixr 90) |
17 "+" :: [nat,nat] => nat (infixr 90) |
18 "<","<=" :: "[nat,nat] => o" (infixr 70) |
18 "<","<=" :: [nat,nat] => o (infixr 70) |
19 |
19 |
20 rules |
20 rules |
21 pred_0 "pred(0) = 0" |
21 pred_0 "pred(0) = 0" |
22 pred_succ "pred(succ(m)) = m" |
22 pred_succ "pred(succ(m)) = m" |
23 |
23 |