# HG changeset patch
# User paulson
# Date 826037715 -3600
# Node ID eacaa07e907809deae42cf7f3ae897edf9acf406
# Parent  f21c8fab7c3c50d04d3a42d384771d700eb3b7f6
Converted TABs to spaces

diff -r f21c8fab7c3c -r eacaa07e9078 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))"