| changeset 41310 | 65631ca437c9 |
| parent 36319 | 8feb2c4bef1a |
| child 41777 | 1f7cbe39d425 |
| 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 (*Proof terms*) |
21 (*Proof terms*) |