src/ZF/Constructible/L_axioms.thy

--- a/src/ZF/Constructible/L_axioms.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1309,7 +1309,7 @@
 subsubsection{*Finite Ordinals: The Predicate ``Is A Natural Number''*}
 
 (*     "finite_ordinal(M,a) == 
-	ordinal(M,a) & ~ limit_ordinal(M,a) & 
+        ordinal(M,a) & ~ limit_ordinal(M,a) & 
         (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))" *)
 definition
   finite_ordinal_fm :: "i=>i" where