author | wenzelm |
Wed, 27 Nov 1996 16:45:57 +0100 | |
changeset 2258 | 8ad8ee759d9f |
parent 2257 | c8154379738c |
child 2259 | e6d738f2b9a9 |
src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Nat.thy Wed Nov 27 16:42:48 1996 +0100 +++ b/src/HOL/Nat.thy Wed Nov 27 16:45:57 1996 +0100 @@ -44,8 +44,6 @@ consts "0" :: nat ("0") - "1" :: nat ("1") - "2" :: nat ("2") Suc :: nat => nat nat_case :: ['a, nat => 'a, nat] => 'a pred_nat :: "(nat * nat) set" @@ -53,6 +51,10 @@ Least :: (nat=>bool) => nat (binder "LEAST " 10) +syntax + "1" :: nat ("1") + "2" :: nat ("2") + translations "1" == "Suc(0)" "2" == "Suc(1)"