diff -r 7be9b054f672 -r c46b6abad24b Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sun Jan 24 23:41:27 2010 +0100
+++ b/Quot/QuotMain.thy	Mon Jan 25 17:53:08 2010 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ??/QuotMain.thy
+(*  Title:      QuotMain.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
@@ -32,6 +32,11 @@
 where
   "rep a = Eps (Rep a)"
 
+text {*
+  The naming of the lemmas follows the quotient paper
+  by Peter Homeier.
+*}
+
 lemma lem9:
   shows "R (Eps (R x)) = R x"
 proof -
@@ -62,12 +67,12 @@
 by (simp add: equivp[simplified equivp_def])
 
 lemma lem7:
-  shows "(R x = R y) = (Abs (R x) = Abs (R y))"
-apply(rule iffI)
-apply(simp)
-apply(drule rep_inject[THEN iffD2])
-apply(simp add: abs_inverse)
-done
+  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)
+  also have "\<dots> = ?LHS" by (simp add: abs_inverse)
+  finally show "?LHS = ?RHS" by simp
+qed
 
 theorem thm11:
   shows "R r r' = (abs r = abs r')"
@@ -81,7 +86,7 @@
 
 lemma Quotient:
   shows "Quotient R abs rep"
-apply(unfold Quotient_def)
+unfolding Quotient_def
 apply(simp add: thm10)
 apply(simp add: rep_refl)
 apply(subst thm11[symmetric])
@@ -90,11 +95,9 @@
 
 end
 
-term Quot_Type.abs
-
 section {* ML setup *}
 
-(* Auxiliary data for the quotient package *)
+text {* Auxiliary data for the quotient package *}
 
 use "quotient_info.ML"
 
@@ -104,34 +107,32 @@
 lemmas [quot_respect] = quot_rel_rsp
 lemmas [quot_equiv] = identity_equivp
 
-(* Lemmas about simplifying id's. *)
+
+text {* Lemmas about simplifying id's. *}
 lemmas [id_simps] =
+  id_def[symmetric, THEN eq_reflection]
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_o[THEN eq_reflection]
-  id_def[symmetric, THEN eq_reflection]
   o_id[THEN eq_reflection]
   eq_comp_r
 
-(* The translation functions for the lifting process. *)
+text {* Translation functions for the lifting process. *}
 use "quotient_term.ML" 
 
 
-(* Definition of the quotient types *)
+text {* Definitions of the quotient types. *}
 use "quotient_typ.ML"
 
 
-(* Definitions for quotient constants *)
+text {* Definitions for quotient constants. *}
 use "quotient_def.ML"
 
-(* Tactics for proving the lifted theorems *)
 
-lemma eq_imp_rel:  
-  "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" 
-by (simp add: equivp_reflp)
-
-(* An auxiliar constant for recording some information *) 
-(* about the lifted theorem in a tactic.               *)
+text {* 
+  An auxiliar constant for recording some information  
+  about the lifted theorem in a tactic.       
+*}
 definition
   "Quot_True x \<equiv> True"
 
@@ -146,6 +147,7 @@
 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"