# HG changeset patch # User traytel # Date 1349162428 -7200 # Node ID 1cf810b8f6004317f518dd67d08ee0c7003bb0c4 # Parent 78a3d5006cf13efd6d08326fce03c4fc2a3c7e10 made tactic more robust (less usage of stac) diff -r 78a3d5006cf1 -r 1cf810b8f600 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue Oct 02 01:00:18 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue Oct 02 09:20:28 2012 +0200 @@ -288,12 +288,12 @@ REPEAT_DETERM o etac conjE, hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], - rtac bexI, rtac conjI, rtac trans, rtac map_comp, - REPEAT_DETERM_N m o stac @{thm id_o}, - REPEAT_DETERM_N n o stac @{thm o_id}, - etac sym, rtac trans, rtac map_comp, - REPEAT_DETERM_N m o stac @{thm id_o}, - REPEAT_DETERM_N n o stac @{thm o_id}, + rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong, + REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), + REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), + etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong, + REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), + REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), rtac trans, rtac map_cong, REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac], REPEAT_DETERM_N n o rtac refl,