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 w.r.t. equations containing 'case_prod'
authorblanchet
Thu, 16 Jul 2015 17:25:44 +0200
changeset 60735 cf291b55f3d1
parent 60728 26ffdb966759
child 60736 c4bc0691860b
made tactic more robust w.r.t. equations containing 'case_prod'
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Jul 16 12:23:22 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Jul 16 17:25:44 2015 +0200
@@ -82,9 +82,11 @@
     etac ctxt notE THEN' atac ORELSE'
     etac ctxt disjE))));
 
-fun ss_fst_snd_conv ctxt = simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
+fun ss_fst_snd_conv ctxt =
+  Raw_Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
 
-fun case_atac ctxt = simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
+fun case_atac ctxt =
+  Simplifier.full_simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
 
 fun same_case_tac ctxt m =
   HEADGOAL (if m = 0 then rtac ctxt TrueI
isabelle