src/ZF/Order.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Order.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Order.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,13 +8,13 @@
     1.4  
     1.5  Order = WF + Perm + 
     1.6  consts
     1.7 -  part_ord        :: "[i,i]=>o"		(*Strict partial ordering*)
     1.8 -  linear, tot_ord :: "[i,i]=>o"		(*Strict total ordering*)
     1.9 -  well_ord        :: "[i,i]=>o"		(*Well-ordering*)
    1.10 -  mono_map        :: "[i,i,i,i]=>i"	(*Order-preserving maps*)
    1.11 -  ord_iso         :: "[i,i,i,i]=>i"	(*Order isomorphisms*)
    1.12 -  pred            :: "[i,i,i]=>i"	(*Set of predecessors*)
    1.13 -  ord_iso_map     :: "[i,i,i,i]=>i"	(*Construction for linearity theorem*)
    1.14 +  part_ord        :: [i,i]=>o		(*Strict partial ordering*)
    1.15 +  linear, tot_ord :: [i,i]=>o		(*Strict total ordering*)
    1.16 +  well_ord        :: [i,i]=>o		(*Well-ordering*)
    1.17 +  mono_map        :: [i,i,i,i]=>i	(*Order-preserving maps*)
    1.18 +  ord_iso         :: [i,i,i,i]=>i	(*Order isomorphisms*)
    1.19 +  pred            :: [i,i,i]=>i	(*Set of predecessors*)
    1.20 +  ord_iso_map     :: [i,i,i,i]=>i	(*Construction for linearity theorem*)
    1.21  
    1.22  defs
    1.23    part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"