src/ZF/Order.thy
 changeset 1401 0c439768f45c parent 1155 928a16e02f9f child 1478 2b8c2a7547ab
```--- 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)"```