changeset 41310 | 65631ca437c9 |
parent 35762 | af3ff2ba4c54 |
child 51309 | 473303ef6e34 |
--- a/src/Sequents/LK/Nat.thy Mon Dec 20 15:24:25 2010 +0100 +++ b/src/Sequents/LK/Nat.thy Mon Dec 20 16:44:33 2010 +0100 @@ -11,7 +11,7 @@ typedecl nat arities nat :: "term" -consts "0" :: nat ("0") +consts Zero :: nat ("0") Suc :: "nat=>nat" rec :: "[nat, 'a, [nat,'a]=>'a] => 'a" add :: "[nat, nat] => nat" (infixl "+" 60)