# HG changeset patch # User wenzelm # Date 849109557 -3600 # Node ID 8ad8ee759d9fba34967a914e05f366d833cb4c12 # Parent c8154379738c136269d3d042f64aa45ddfb29529 moved "1", "2" to syntax section; diff -r c8154379738c -r 8ad8ee759d9f src/HOL/Nat.thy --- 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)"