src/HOL/Nat.thy
changeset 1824 44254696843a
parent 1674 33aff4d854e4
child 2258 8ad8ee759d9f
     1.1 --- a/src/HOL/Nat.thy	Fri Jun 21 13:51:09 1996 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Jun 25 13:11:29 1996 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4    Suc       :: nat => nat
     1.5    nat_case  :: ['a, nat => 'a, nat] => 'a
     1.6    pred_nat  :: "(nat * nat) set"
     1.7 -  nat_rec   :: [nat, 'a, [nat, 'a] => 'a] => 'a
     1.8 +  nat_rec   :: ['a, [nat, 'a] => 'a, nat] => 'a
     1.9  
    1.10    Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    1.11  
    1.12 @@ -71,8 +71,8 @@
    1.13  
    1.14    le_def        "m<=(n::nat) == ~(n<m)"
    1.15  
    1.16 -  nat_rec_def   "nat_rec n c d ==
    1.17 -                 wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
    1.18 +  nat_rec_def   "nat_rec c d ==
    1.19 +                 wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
    1.20    (*least number operator*)
    1.21    Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
    1.22