src/HOL/Nat.thy
changeset 1475 7f5a4cd08209
parent 1370 7361ac9b024d
child 1531 e5eb247ad13c
     1.1 --- a/src/HOL/Nat.thy	Mon Feb 05 14:44:09 1996 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Feb 05 21:27:16 1996 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  (* type definition *)
     1.6  
     1.7 -subtype (Nat)
     1.8 +typedef (Nat)
     1.9    nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
    1.10  
    1.11  instance
    1.12 @@ -65,6 +65,5 @@
    1.13  
    1.14    le_def   "m<=(n::nat) == ~(n<m)"
    1.15  
    1.16 -  nat_rec_def   "nat_rec n c d == wfrec pred_nat n  
    1.17 -                        (nat_case (%g.c) (%m g.(d m (g m))))"
    1.18 +nat_rec_def"nat_rec n c d == wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
    1.19  end