diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Sprod1.thy
--- a/src/HOLCF/Sprod1.thy	Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Sprod1.thy	Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOLCF/sprod1.thy
+(*  Title:      HOLCF/sprod1.thy
     ID:         $Id$
-    Author: 	Franz Regensburger
+    Author:     Franz Regensburger
     Copyright   1993  Technische Universitaet Muenchen
 
 Partial ordering for the strict product
@@ -9,12 +9,12 @@
 Sprod1 = Sprod0 +
 
 consts
-  less_sprod	:: "[('a ** 'b),('a ** 'b)] => bool"	
+  less_sprod    :: "[('a ** 'b),('a ** 'b)] => bool"    
 
 defs
   less_sprod_def "less_sprod p1 p2 == 
-	if p1 = Ispair UU UU
-		then True
-		else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
+        if p1 = Ispair UU UU
+                then True
+                else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
 
 end