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.
strengthened tactic
authorblanchet
Mon, 07 Mar 2016 23:20:11 +0100
changeset 62535 cb262f03ac12
parent 62534 6855b348e828
child 62536 656e9653c645
strengthened tactic
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Mar 07 15:57:02 2016 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Mar 07 23:20:11 2016 +0100
@@ -117,8 +117,8 @@
 fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =
   HEADGOAL Goal.conjunction_tac THEN
   ALLGOALS (REPEAT o (resolve_tac ctxt (rel_funI :: rel_intros) THEN'
-    TRY o (REPEAT_DETERM1 o (assume_tac ctxt ORELSE'
-      K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac ctxt refl))));
+    TRY o (REPEAT_DETERM1 o (SELECT_GOAL (unfold_thms_tac ctxt rel_eqs) THEN'
+      (assume_tac ctxt ORELSE' hyp_subst_tac ctxt THEN' rtac ctxt refl)))));
 
 fun mk_disc_transfer_tac ctxt rel_sel exhaust_disc distinct_disc =
   let
isabelle