src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Thu Mar 28 10:56:10 1996 +0100
+++ b/src/HOL/Nat.thy	Thu Mar 28 12:25:55 1996 +0100
@@ -44,6 +44,8 @@
 
 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"
@@ -52,6 +54,8 @@
   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
 
 translations
+   "1"  == "Suc(0)"
+   "2"  == "Suc(1)"
   "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
 
 defs