src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Tue Mar 05 15:52:59 1996 +0100
+++ b/src/HOL/Nat.thy	Tue Mar 05 15:55:15 1996 +0100
@@ -68,7 +68,7 @@
   le_def        "m<=(n::nat) == ~(n<m)"
 
   nat_rec_def   "nat_rec n c d ==
-		 wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
+                 wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
   (*least number operator*)
   Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"