src/HOL/ex/LexProd.thy

--- a/src/HOL/ex/LexProd.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/LexProd.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/lex-prod.thy
+(*  Title:      HOL/ex/lex-prod.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow, TU Munich
+    Author:     Tobias Nipkow, TU Munich
     Copyright   1993  TU Munich
 
 The lexicographic product of two relations.
@@ -10,6 +10,6 @@
 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)}"
+        p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
 end