# HG changeset patch # User traytel # Date 1513496579 -3600 # Node ID 19809bc9d7ffcd5b5b09ae747219ed48285782d9 # Parent 62a5fbdded50d03a07bf74937a01a55f42e342c8 made tactics more robust diff -r 62a5fbdded50 -r 19809bc9d7ff src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Sat Dec 16 22:32:04 2017 +0100 +++ b/src/HOL/Tools/BNF/bnf_def.ML Sun Dec 17 08:42:59 2017 +0100 @@ -1904,7 +1904,8 @@ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => HEADGOAL (rtac ctxt (pred_set RSN (2, pred_set RSN (2, box_equals)))) THEN - unfold_thms_tac ctxt (@{thm Ball_image_comp} :: map Lazy.force set_map) THEN + unfold_thms_tac ctxt + (@{thms Ball_image_comp ball_empty} @ map Lazy.force set_map) THEN HEADGOAL (rtac ctxt refl)) |> Thm.close_derivation end; diff -r 62a5fbdded50 -r 19809bc9d7ff src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Sat Dec 16 22:32:04 2017 +0100 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Sun Dec 17 08:42:59 2017 +0100 @@ -259,8 +259,11 @@ (HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) :: @{thms exE conjE CollectE}))) THEN - HEADGOAL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt rel_map THEN HEADGOAL (rtac ctxt iffI) THEN - last_tac iffD1 THEN last_tac iffD2) + HEADGOAL (hyp_subst_tac ctxt) THEN + REPEAT_DETERM (HEADGOAL (resolve_tac ctxt (maps (fn thm => + [thm RS trans, thm RS @{thm trans[rotated, OF sym]}]) rel_map))) THEN + HEADGOAL (rtac ctxt iffI) THEN + last_tac iffD1 THEN print_tac ctxt "baz" THEN last_tac iffD2) end; fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =