--- a/Quot/QuotOption.thy	Tue Jan 26 10:53:44 2010 +0100
+++ b/Quot/QuotOption.thy	Tue Jan 26 11:13:08 2010 +0100
@@ -5,7 +5,7 @@
 imports QuotMain
 begin
 
-section {* Quotient infrastructure for option type *}
+section {* Quotient infrastructure for the option type. *}
 
 fun
   option_rel
@@ -20,10 +20,10 @@
 text {* should probably be in Option.thy *}
 lemma split_option_all: 
   shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
-apply(auto)
-apply(case_tac x)
-apply(simp_all)
-done
+  apply(auto)
+  apply(case_tac x)
+  apply(simp_all)
+  done
 
 lemma option_quotient[quot_thm]:
   assumes q: "Quotient R Abs Rep"