1.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Aug 18 22:31:52 2011 -0700
1.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Aug 18 22:32:19 2011 -0700
1.3 @@ -168,7 +168,7 @@
1.4 val eq_eqvs = eq_imp_rel_get ctxt
1.5 in
1.6 simp_tac simpset THEN'
1.7 - REPEAT_ALL_NEW (CHANGED o FIRST'
1.8 + TRY o REPEAT_ALL_NEW (CHANGED o FIRST'
1.9 [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
1.10 resolve_tac (Inductive.get_monos ctxt),
1.11 resolve_tac @{thms ball_all_comm bex_ex_comm},
1.12 @@ -396,12 +396,12 @@
1.13 Cong_Tac.cong_tac @{thm cong} THEN'
1.14 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
1.15
1.16 + (* resolving with R x y assumptions *)
1.17 + atac,
1.18 +
1.19 (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
1.20 rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
1.21
1.22 - (* resolving with R x y assumptions *)
1.23 - atac,
1.24 -
1.25 (* reflexivity of the basic relations *)
1.26 (* R ... ... *)
1.27 resolve_tac rel_refl]