--- a/Quot/QuotSum.thy	Tue Jan 26 10:53:44 2010 +0100
+++ b/Quot/QuotSum.thy	Tue Jan 26 11:13:08 2010 +0100
@@ -5,6 +5,8 @@
 imports QuotMain
 begin
 
+section {* Quotient infrastructure for the sum type. *}
+
 fun
   sum_rel
 where
@@ -25,10 +27,10 @@
 text {* should probably be in Sum_Type.thy *}
 lemma split_sum_all: 
   shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
-apply(auto)
-apply(case_tac x)
-apply(simp_all)
-done
+  apply(auto)
+  apply(case_tac x)
+  apply(simp_all)
+  done
 
 lemma sum_equivp[quot_equiv]:
   assumes a: "equivp R1"