changeset 41558 | 65631ca437c9 |
parent 35762 | af3ff2ba4c54 |
child 52446 | 473303ef6e34 |
1.1 --- a/src/Sequents/LK/Nat.thy Mon Dec 20 15:24:25 2010 +0100 1.2 +++ b/src/Sequents/LK/Nat.thy Mon Dec 20 16:44:33 2010 +0100 1.3 @@ -11,7 +11,7 @@ 1.4 1.5 typedecl nat 1.6 arities nat :: "term" 1.7 -consts "0" :: nat ("0") 1.8 +consts Zero :: nat ("0") 1.9 Suc :: "nat=>nat" 1.10 rec :: "[nat, 'a, [nat,'a]=>'a] => 'a" 1.11 add :: "[nat, nat] => nat" (infixl "+" 60)