diff -r a95f6bb081cf -r d6acae26d027 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 22 07:42:16 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 22 20:51:37 2009 +0100
@@ -74,14 +74,13 @@
 unfolding abs_def
 by (simp only: equivp[simplified equivp_def] lem7)
 
-
 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)
 
 lemma Quotient:
-  "Quotient R abs rep"
+  shows "Quotient R abs rep"
 apply(unfold Quotient_def)
 apply(simp add: thm10)
 apply(simp add: rep_refl)
@@ -91,56 +90,65 @@
 
 end
 
-section {* type definition for the quotient type *}
 
-(* auxiliary data for the quotient package *)
+section {* ML setup *}
+
+(* Auxiliary data for the quotient package *)
 use "quotient_info.ML"
 
 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 *)
 lemmas [quot_equiv] = identity_equivp
 
-(* definition of the quotient types *)
+(* Lemmas about simplifying id's. *)
+lemmas [id_simps] =
+  fun_map_id[THEN eq_reflection]
+  id_apply[THEN eq_reflection]
+  id_def[THEN eq_reflection, symmetric]
+  id_o[THEN eq_reflection]
+  o_id[THEN eq_reflection] 
+
+(* Definition of the quotient types *)
 use "quotient_typ.ML"
 
-(* lifting of constants *)
+
+(* Definitions for quotient constants *)
 use "quotient_def.ML"
 
-(* the translation functions for the lifting process *)
+
+(* The translation functions for the lifting process. *)
 use "quotient_term.ML" 
 
-(* tactics for proving the theorems *)
+
+(* Tactics for proving the lifted theorems *)
 
 lemma eq_imp_rel:  
-  "equivp R ==> a = b \<longrightarrow> R a b" 
+  "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" 
 by (simp add: equivp_reflp)
 
-(* an auxiliar constant that records some information *) 
-(* about the lifted theorem                           *)
+(* An auxiliar constant for recording some information *) 
+(* about the lifted theorem in a tactic.               *)
 definition
-  "QUOT_TRUE x \<equiv> True"
+  "Quot_True x \<equiv> True"
 
-lemma quot_true_dests:
-  shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
-  and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
-  and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
-  and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
-by (simp_all add: QUOT_TRUE_def ext)
+lemma 
+  shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
+  and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
+  and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True  (P x))"
+  and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
+by (simp_all add: Quot_True_def ext)
 
-lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
-by (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)
+lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
+by (simp add: Quot_True_def)
 
 use "quotient_tacs.ML"
 
-(* atomize infrastructure *)
+
+(* Atomize infrastructure *)
+(* FIXME/TODO: is this really needed? *)
+(*
 lemma atomize_eqv[atomize]:
   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
 proof
@@ -160,15 +168,7 @@
   qed
   then show "A \<equiv> B" by (rule eq_reflection)
 qed
-
-(* 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_o[THEN eq_reflection]
-  o_id[THEN eq_reflection] 
-
+*)
 
 section {* Methods / Interface *}
 
@@ -193,7 +193,7 @@
   {* Proves automatically the regularization goals from the lifting procedure. *}
 
 method_setup injection =
-  {* Scan.succeed (mk_method2 Quotient_Tacs.all_inj_repabs_tac) *}
+  {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
   {* Proves automatically the rep/abs injection goals from the lifting procedure. *}
 
 method_setup cleaning =