changeset 49946 | a69ec82ffae6 |
parent 49944 | 28cd3c9ca278 |
child 49957 | 6250121bfffb |
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Sat Oct 20 09:09:34 2012 +0200 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML Sat Oct 20 09:09:35 2012 +0200 @@ -241,7 +241,7 @@ val elim_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]} THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE})) - THEN' TRY o etac @{thm conjE} + THEN' REPEAT_DETERM o etac @{thm conjE} THEN' TRY o hyp_subst_tac; fun intro_image_tac ctxt = rtac @{thm image_eqI}