diff -r 5c6d76c3ba5c -r f537d570fff8 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Jan 13 16:23:32 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 13 16:39:20 2010 +0100
@@ -51,16 +51,12 @@
 
 (** solvers for equivp and quotient assumptions **)
 
-(* FIXME / TODO: should this SOLVED' the goal, like with quotient_tac? *)
-(* FIXME / TODO: none of te examples break if added                    *)
 fun equiv_tac ctxt =
   REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
 
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
-(* FIXME / TODO: test whether DETERM makes any runtime-difference *)
-(* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *)
 fun quotient_tac ctxt = SOLVED'
   (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
@@ -279,8 +275,6 @@
       end
   | _ => K no_tac
 end
-(* TODO: Again, can one specify more concretely        *)
-(* TODO: in terms of R when no_tac should be returned? *)
 
 fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>