| 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)