diff -r 6055775a151b -r f4d16517b360 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Aug 06 18:21:14 1998 +0200
+++ b/src/HOL/List.thy	Sat Aug 08 14:00:56 1998 +0200
@@ -145,6 +145,22 @@
   replicate_0   "replicate 0 x       = []"
   replicate_Suc "replicate (Suc n) x = x # replicate n x"
 
+(** Lexcicographic orderings on lists **)
+
+consts
+ lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
+primrec
+"lexn r 0       = {}"
+"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r ** lexn r n)) Int
+                  {(xs,ys). length xs = Suc n & length ys = Suc n}"
+
+constdefs
+ lex :: "('a * 'a)set => ('a list * 'a list)set"
+"lex r == UN n. lexn r n"
+
+ lexico :: "('a * 'a)set => ('a list * 'a list)set"
+"lexico r == inv_image (less_than ** lex r) (%xs. (length xs, xs))"
+
 end
 
 ML