--- a/QuotMain.thy	Thu Nov 26 20:32:33 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 20:32:56 2009 +0100
@@ -894,11 +894,8 @@
 
 
 
-(****************************************)
-(* cleaning of the theorem              *)
-(****************************************)
 
-
+section {* Cleaning of the theorem *}
 
 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
 ML {*