diff -r 3104d62e7a16 -r 119f7d6a3556 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 17 14:58:33 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 17 17:59:12 2009 +0100
@@ -1,3 +1,7 @@
+(*  Title:      ??/QuotMain.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+*)
+
 theory QuotMain
 imports QuotScript Prove
 uses ("quotient_info.ML")
@@ -89,15 +93,12 @@
 
 section {* type definition for the quotient type *}
 
-(* the auxiliary data for the quotient types *)
+(* auxiliary data for the quotient package *)
 use "quotient_info.ML"
 
-ML {* print_mapsinfo @{context} *}
-
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient 
-
 lemmas [quot_respect] = quot_rel_rsp
 
 (* fun_map is not here since equivp is not true *)
@@ -109,14 +110,17 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
-(* the translation functions *)
+(* the translation functions for the lifting process *)
 use "quotient_term.ML" 
 
-(* tactics *)
+(* tactics for proving the theorems *)
+
 lemma eq_imp_rel:  
-  "equivp R ==> a = b --> R a b" 
+  "equivp R ==> a = b \<longrightarrow> R a b" 
 by (simp add: equivp_reflp)
 
+(* an auxiliar constant that records some information *) 
+(* about the lifted theorem                           *)
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -130,13 +134,13 @@
 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
 by (simp add: QUOT_TRUE_def)
 
-lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
-  by(auto simp add: QUOT_TRUE_def)
+lemma regularize_to_injection: 
+  shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
+by(auto simp add: QUOT_TRUE_def)
 
 use "quotient_tacs.ML"
 
-section {* Atomize Infrastructure *}
-
+(* atomize infrastructure *)
 lemma atomize_eqv[atomize]:
   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
 proof
@@ -157,12 +161,11 @@
   then show "A \<equiv> B" by (rule eq_reflection)
 qed
 
-section {* Infrastructure about id *}
-
+(* lemmas about simplifying id *)
 lemmas [id_simps] =
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
-  id_def[THEN eq_reflection,symmetric]
+  id_def[THEN eq_reflection, symmetric]
 
 section {* Methods / Interface *}