--- a/src/ZF/Order.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Order.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,13 +8,13 @@
Order = WF + Perm +
consts
- part_ord :: "[i,i]=>o" (*Strict partial ordering*)
- linear, tot_ord :: "[i,i]=>o" (*Strict total ordering*)
- 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*)
- ord_iso_map :: "[i,i,i,i]=>i" (*Construction for linearity theorem*)
+ part_ord :: [i,i]=>o (*Strict partial ordering*)
+ linear, tot_ord :: [i,i]=>o (*Strict total ordering*)
+ 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*)
+ ord_iso_map :: [i,i,i,i]=>i (*Construction for linearity theorem*)
defs
part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"