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.
made tactic more robust (less usage of stac)
authortraytel
Tue, 02 Oct 2012 09:20:28 +0200
changeset 49684 1cf810b8f600
parent 49683 78a3d5006cf1
child 49685 4341e4d86872
made tactic more robust (less usage of stac)
src/HOL/BNF/Tools/bnf_gfp_tactics.ML file | annotate | diff | comparison | revisions 
--- 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,
isabelle