# HG changeset patch
# User paulson
# Date 837091690 -7200
# Node ID 7b1e1c298e50d667d4577a44eecdec3e89cfcacd
# Parent  c6b6ccfd390c7a3b56fccf9bc6dc45930e063be8
Corrected indentation

diff -r c6b6ccfd390c -r 7b1e1c298e50 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