src/ZF/Order.thy
changeset 1851 7b1e1c298e50
parent 1478 2b8c2a7547ab
child 2469 b50b8c0eec01
     1.1 --- a/src/ZF/Order.thy	Thu Jul 11 15:18:57 1996 +0200
     1.2 +++ b/src/ZF/Order.thy	Thu Jul 11 15:28:10 1996 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    well_ord        :: [i,i]=>o           (*Well-ordering*)
     1.5    mono_map        :: [i,i,i,i]=>i       (*Order-preserving maps*)
     1.6    ord_iso         :: [i,i,i,i]=>i       (*Order isomorphisms*)
     1.7 -  pred            :: [i,i,i]=>i (*Set of predecessors*)
     1.8 +  pred            :: [i,i,i]=>i		(*Set of predecessors*)
     1.9    ord_iso_map     :: [i,i,i,i]=>i       (*Construction for linearity theorem*)
    1.10  
    1.11  defs