--- a/Quot/QuotProd.thy	Tue Jan 26 10:53:44 2010 +0100
+++ b/Quot/QuotProd.thy	Tue Jan 26 11:13:08 2010 +0100
@@ -5,7 +5,7 @@
 imports QuotMain
 begin
 
-section {* Quotient infrastructure for product type *}
+section {* Quotient infrastructure for the product type. *}
 
 fun
   prod_rel
@@ -44,7 +44,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
-by simp
+  by simp
 
 lemma Pair_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"