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.
try tactics in right order w.r.t. schematics
authorblanchet
Tue, 29 Mar 2016 18:32:08 +0200
changeset 62744 b4f139bf02e3
parent 62743 f9a65b48f5e2
child 62745 257a022f7e7b
try tactics in right order w.r.t. schematics
src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Tue Mar 29 18:07:55 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Tue Mar 29 18:32:08 2016 +0200
@@ -67,8 +67,8 @@
     rtac ctxt cong_alg_intro) THEN
   unfold_thms_tac ctxt (extra_simps @ sumprod_thms_rel @
     @{thms vimage2p_def prod.rel_eq sum.rel_eq}) THEN
-  REPEAT_DETERM (HEADGOAL (etac ctxt subst ORELSE' rtac ctxt conjI ORELSE' assume_tac ctxt ORELSE'
-    rtac ctxt refl));
+  REPEAT_DETERM (HEADGOAL (rtac ctxt conjI ORELSE' assume_tac ctxt ORELSE' rtac ctxt refl ORELSE'
+    etac ctxt subst));
 
 val shared_simps =
   @{thms map_prod_simp map_sum.simps sum.case prod.case_eq_if split_beta' prod.sel
isabelle