# HG changeset patch
# User wenzelm
# Date 881062862 -3600
# Node ID 9849fb57c395c2fb292f1ce2e629e24deadf2466
# Parent  472e2df01d3329c835a81527055bb0efbb8e2522
added prod_ord, dict_ord, list_ord;

diff -r 472e2df01d33 -r 9849fb57c395 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Dec 02 12:40:06 1997 +0100
+++ b/src/Pure/library.ML	Tue Dec 02 12:41:02 1997 +0100
@@ -721,16 +721,31 @@
 
 datatype order = LESS | EQUAL | GREATER;
 
-fun intord (i, j: int) =
+fun int_ord (i, j: int) =
   if i < j then LESS
   else if i = j then EQUAL
   else GREATER;
 
-fun stringord (a, b: string) =
+fun string_ord (a, b: string) =
   if a < b then LESS
   else if a = b then EQUAL
   else GREATER;
 
+(*lexicographic product*)
+fun prod_ord a_ord b_ord ((x, y), (x', y')) =
+  (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord);
+
+(*dictionary order -- in general NOT well-founded!*)
+fun dict_ord _ ([], []) = EQUAL
+  | dict_ord _ ([], _ :: _) = LESS
+  | dict_ord _ (_ :: _, []) = GREATER
+  | dict_ord elem_ord (x :: xs, y :: ys) =
+      (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord);
+
+(*lexicographic product of lists*)
+fun list_ord elem_ord (xs, ys) =
+  prod_ord int_ord (dict_ord elem_ord) ((length xs, xs), (length ys, ys));
+
 
 
 (** input / output and diagnostics **)