changeset 1322 | 9b3d3362a048 |
parent 352 | fd3ab8bcb69d |
child 1473 | e8d4606e6502 |
--- a/src/FOL/ex/Nat2.thy Tue Nov 07 12:57:20 1995 +0100 +++ b/src/FOL/ex/Nat2.thy Tue Nov 07 12:58:17 1995 +0100 @@ -12,10 +12,10 @@ arities nat :: term consts - succ,pred :: "nat => nat" - "0" :: "nat" ("0") - "+" :: "[nat,nat] => nat" (infixr 90) - "<","<=" :: "[nat,nat] => o" (infixr 70) + succ,pred :: nat => nat + "0" :: nat ("0") + "+" :: [nat,nat] => nat (infixr 90) + "<","<=" :: [nat,nat] => o (infixr 70) rules pred_0 "pred(0) = 0"