--- a/Quot/QuotMain.thy	Wed Feb 10 12:30:26 2010 +0100
+++ b/Quot/QuotMain.thy	Wed Feb 10 17:02:29 2010 +0100
@@ -4,11 +4,12 @@
 
 theory QuotMain
 imports QuotBase
-uses ("quotient_info.ML")
-     ("quotient_typ.ML")
-     ("quotient_def.ML")
-     ("quotient_term.ML")
-     ("quotient_tacs.ML")
+uses
+  ("quotient_info.ML")
+  ("quotient_typ.ML")
+  ("quotient_def.ML")
+  ("quotient_term.ML")
+  ("quotient_tacs.ML")
 begin
 
 locale Quot_Type =
@@ -32,12 +33,7 @@
 where
   "rep a = Eps (Rep a)"
 
-text {*
-  The naming of the lemmas follows the quotient paper
-  by Peter Homeier.
-*}
-
-lemma lem9:
+lemma homeier_lem9:
   shows "R (Eps (R x)) = R x"
 proof -
   have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
@@ -46,21 +42,21 @@
     using equivp unfolding equivp_def by simp
 qed
 
-theorem thm10:
+theorem homeier_thm10:
   shows "abs (rep a) = a"
   unfolding abs_def rep_def
 proof -
   from rep_prop
   obtain x where eq: "Rep a = R x" by auto
   have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
-  also have "\<dots> = Abs (R x)" using lem9 by simp
+  also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
   also have "\<dots> = Abs (Rep a)" using eq by simp
   also have "\<dots> = a" using rep_inverse by simp
   finally
   show "Abs (R (Eps (Rep a))) = a" by simp
 qed
 
-lemma lem7:
+lemma homeier_lem7:
   shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
 proof -
   have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
@@ -68,10 +64,10 @@
   finally show "?LHS = ?RHS" by simp
 qed
 
-theorem thm11:
+theorem homeier_thm11:
   shows "R r r' = (abs r = abs r')"
   unfolding abs_def
-  by (simp only: equivp[simplified equivp_def] lem7)
+  by (simp only: equivp[simplified equivp_def] homeier_lem7)
 
 lemma rep_refl:
   shows "R (rep a) (rep a)"
@@ -82,14 +78,14 @@
 lemma rep_abs_rsp:
   shows "R f (rep (abs g)) = R f g"
   and   "R (rep (abs g)) f = R g f"
-  by (simp_all add: thm10 thm11)
+  by (simp_all add: homeier_thm10 homeier_thm11)
 
 lemma Quotient:
   shows "Quotient R abs rep"
   unfolding Quotient_def
-  apply(simp add: thm10)
+  apply(simp add: homeier_thm10)
   apply(simp add: rep_refl)
-  apply(subst thm11[symmetric])
+  apply(subst homeier_thm11[symmetric])
   apply(simp add: equivp[simplified equivp_def])
   done
 
@@ -129,9 +125,9 @@
 use "quotient_def.ML"
 
 
-text {* 
-  An auxiliar constant for recording some information  
-  about the lifted theorem in a tactic.       
+text {*
+  An auxiliary constant for recording some information
+  about the lifted theorem in a tactic.
 *}
 definition
   "Quot_True x \<equiv> True"
@@ -147,11 +143,13 @@
 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
   by (simp add: Quot_True_def)
 
+
 text {* Tactics for proving the lifted theorems *}
 use "quotient_tacs.ML"
 
 section {* Methods / Interface *}
 
+(* TODO inline *)
 ML {*
 fun mk_method1 tac thms ctxt =
   SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) 
@@ -162,27 +160,27 @@
 
 method_setup lifting =
   {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *}
-  {* Lifting of theorems to quotient types. *}
+  {* lifts theorems to quotient types *}
 
 method_setup lifting_setup =
   {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
-  {* Sets up the three goals for the lifting procedure. *}
+  {* sets up the three goals for the quotient lifting procedure *}
 
 method_setup regularize =
   {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
-  {* Proves automatically the regularization goals from the lifting procedure. *}
+  {* proves the regularization goals from the quotient lifting procedure *}
 
 method_setup injection =
   {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
-  {* Proves automatically the rep/abs injection goals from the lifting procedure. *}
+  {* proves the rep/abs injection goals from the quotient lifting procedure *}
 
 method_setup cleaning =
   {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
-  {* Proves automatically the cleaning goals from the lifting procedure. *}
+  {* proves the cleaning goals from the quotient lifting procedure *}
 
 attribute_setup quot_lifted =
   {* Scan.succeed Quotient_Tacs.lifted_attrib *}
-  {* Lifting of theorems to quotient types. *}
+  {* lifts theorems to quotient types *}
 
 end