--- a/QuotMain.thy	Thu Nov 26 19:51:31 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 20:18:36 2009 +0100
@@ -885,11 +885,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 {*