diff -r 000000000000 -r 7949f97df77a ex/LexProd.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/LexProd.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,15 @@
+(*  Title: 	HOL/ex/lex-prod.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow, TU Munich
+    Copyright   1993  TU Munich
+
+The lexicographic product of two relations.
+*)
+
+LexProd = WF + Prod +
+consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
+rules
+lex_prod_def "ra**rb == {p. ? a a' b b'. \
+\	p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb)}"
+end
+