--- a/src/Pure/library.ML Sat Aug 03 16:17:16 2019 +0200
+++ b/src/Pure/library.ML Sat Aug 03 20:30:24 2019 +0200
@@ -8,6 +8,7 @@
See also General/basics.ML for the most fundamental concepts.
*)
+infixr 0 <<<
infix 2 ?
infix 3 o oo ooo oooo
infix 4 ~~ upto downto
@@ -196,6 +197,7 @@
val string_ord: string * string -> order
val fast_string_ord: string * string -> order
val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
+ val <<< : ('a -> order) * ('a -> order) -> 'a -> order
val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
@@ -904,6 +906,9 @@
| rev_order EQUAL = EQUAL
| rev_order GREATER = LESS;
+(*compose orders*)
+fun (a_ord <<< b_ord) p = (case a_ord p of EQUAL => b_ord p | ord => ord);
+
(*assume rel is a linear strict order*)
fun make_ord rel (x, y) =
if rel (x, y) then LESS