diff -r c3913a79b6ae -r 492493334e0f ex/LexProd.thy
--- a/ex/LexProd.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/LexProd.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -9,7 +9,7 @@
 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)}"
+lex_prod_def "ra**rb == {p. ? a a' b b'. 
+	p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb)}"
 end