Corrected indentation
authorpaulson
Thu, 11 Jul 1996 15:28:10 +0200
changeset 1851 7b1e1c298e50
parent 1850 c6b6ccfd390c
child 1852 289ce6cb5c84
Corrected indentation
src/ZF/Order.thy
--- a/src/ZF/Order.thy	Thu Jul 11 15:18:57 1996 +0200
+++ b/src/ZF/Order.thy	Thu Jul 11 15:28:10 1996 +0200
@@ -13,7 +13,7 @@
   well_ord        :: [i,i]=>o           (*Well-ordering*)
   mono_map        :: [i,i,i,i]=>i       (*Order-preserving maps*)
   ord_iso         :: [i,i,i,i]=>i       (*Order isomorphisms*)
-  pred            :: [i,i,i]=>i (*Set of predecessors*)
+  pred            :: [i,i,i]=>i		(*Set of predecessors*)
   ord_iso_map     :: [i,i,i,i]=>i       (*Construction for linearity theorem*)
 
 defs