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
authorblanchet
Thu, 02 Jan 2014 21:35:21 +0100
changeset 54918 790362e13e0d
parent 54917 a426e38a8a7e
child 54919 7fad0747e40f
made tactic more robust
src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 20:51:09 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 21:35:21 2014 +0100
@@ -85,8 +85,8 @@
           if Thm.eq_thm (fun_disc', fun_disc) then
             REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
           else
-            rtac FalseE THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN'
-            DETERM o (dresolve_tac disc_excludes THEN' etac notE THEN' atac))
+            rtac FalseE THEN' rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN'
+            dresolve_tac disc_excludes THEN' etac notE THEN' atac)
       fun_discss) THEN'
     rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac);
isabelle