--- a/Quot/QuotList.thy	Wed Dec 09 16:44:34 2009 +0100
+++ b/Quot/QuotList.thy	Wed Dec 09 17:05:33 2009 +0100
@@ -156,10 +156,7 @@
 apply simp_all
 done
 
-(* TODO: induct_tac doesn't accept 'arbitrary'.
-         induct     doesn't accept 'rule'.
-   that's why the proof uses manual generalisation and needs assumptions
-   both in conclusion for induction and in assumptions. *)
+(* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
 lemma foldl_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"

--- a/Quot/QuotMain.thy	Wed Dec 09 16:44:34 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 17:05:33 2009 +0100
@@ -149,7 +149,6 @@
 lemmas [quot_respect] = quot_rel_rsp
 
 (* fun_map is not here since equivp is not true *)
-(* TODO: option, ... *)
 lemmas [quot_equiv] = identity_equivp
 
 (* definition of the quotient types *)
@@ -208,15 +207,10 @@
 
 section {* Infrastructure about id *}
 
-(* TODO: think where should this be *)
-lemma prod_fun_id: "prod_fun id id \<equiv> id"
-  by (rule eq_reflection) (simp add: prod_fun_def)
-
-lemmas [id_simps] = 
+lemmas [id_simps] =
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
-  prod_fun_id
 
 section {* Debugging infrastructure for testing tactics *}
 
@@ -650,21 +644,6 @@
 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
 *}
 
-(* Not used *)
-(* It proves the Quotient assumptions by calling quotient_tac *)
-ML {*
-fun solve_quotient_assum i ctxt thm =
-  let
-    val tac =
-      (compose_tac (false, thm, i)) THEN_ALL_NEW
-      (quotient_tac ctxt);
-    val gc = Drule.strip_imp_concl (cprop_of thm);
-  in
-    Goal.prove_internal [] gc (fn _ => tac 1)
-  end
-  handle _ => error "solve_quotient_assum"
-*}
-
 definition
   "QUOT_TRUE x \<equiv> True"
 

--- a/Quot/QuotProd.thy	Wed Dec 09 16:44:34 2009 +0100
+++ b/Quot/QuotProd.thy	Wed Dec 09 17:05:33 2009 +0100
@@ -90,6 +90,8 @@
   shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p"
 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2])
 
+lemma prod_fun_id[id_simps]: "prod_fun id id \<equiv> id"
+  by (rule eq_reflection) (simp add: prod_fun_def)
 
 section {* general setup for products *}