| changeset 41310 | 65631ca437c9 |
| parent 31974 | e81979a703a4 |
| child 41779 | a68f503805ed |
| 41309:2e9bf718a7a1 | 41310:65631ca437c9 |
|---|---|
11 |
11 |
12 typedecl nat |
12 typedecl nat |
13 arities nat :: "term" |
13 arities nat :: "term" |
14 |
14 |
15 consts |
15 consts |
16 0 :: nat ("0") |
16 Zero :: nat ("0") |
17 Suc :: "nat => nat" |
17 Suc :: "nat => nat" |
18 rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" |
18 rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" |
19 add :: "[nat, nat] => nat" (infixl "+" 60) |
19 add :: "[nat, nat] => nat" (infixl "+" 60) |
20 |
20 |
21 axioms |
21 axioms |