diff -r 50abca9d4043 -r 965127966331 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Jan 13 13:20:32 1997 +0100
+++ b/src/Pure/library.ML	Mon Jan 13 18:20:35 1997 +0100
@@ -5,7 +5,7 @@
 
 Basic library: functions, options, pairs, booleans, lists, integers,
 strings, lists as sets, association lists, generic tables, balanced trees,
-input / output, timing, filenames, misc functions.
+orders, input / output, timing, filenames, misc functions.
 *)
 
 infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
@@ -689,6 +689,22 @@
 
 
 
+(** orders **)
+
+datatype order = LESS | EQUAL | GREATER;
+
+fun intord (i, j: int) =
+  if i < j then LESS
+  else if i = j then EQUAL
+  else GREATER;
+
+fun stringord (a, b: string) =
+  if a < b then LESS
+  else if a = b then EQUAL
+  else GREATER;
+
+
+
 (** input / output **)
 
 val cd = OS.FileSys.chDir;