Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
improving tactic in setcomprehension_simproc
authorbulwahn
Sat, 20 Oct 2012 09:09:35 +0200
changeset 49946 a69ec82ffae6
parent 49945 fb696ff1f086
child 49947 29cd291bfea6
improving tactic in setcomprehension_simproc
src/HOL/Tools/set_comprehension_pointfree.ML file | annotate | diff | comparison | revisions 
--- 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}
isabelle