src/HOL/Nat.thy
changeset 1625 40501958d0f6
parent 1540 eacaa07e9078
child 1660 8cb42cd97579
     1.1 --- a/src/HOL/Nat.thy	Thu Mar 28 10:56:10 1996 +0100
     1.2 +++ b/src/HOL/Nat.thy	Thu Mar 28 12:25:55 1996 +0100
     1.3 @@ -44,6 +44,8 @@
     1.4  
     1.5  consts
     1.6    "0"       :: nat                ("0")
     1.7 +  "1"       :: nat                ("1")
     1.8 +  "2"       :: nat                ("2")
     1.9    Suc       :: nat => nat
    1.10    nat_case  :: ['a, nat => 'a, nat] => 'a
    1.11    pred_nat  :: "(nat * nat) set"
    1.12 @@ -52,6 +54,8 @@
    1.13    Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    1.14  
    1.15  translations
    1.16 +   "1"  == "Suc(0)"
    1.17 +   "2"  == "Suc(1)"
    1.18    "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
    1.19  
    1.20  defs