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 N2M tactic more robust
authortraytel
Thu, 10 Apr 2014 09:38:38 +0200
changeset 56486 753b779d070d
parent 56485 008634379465
child 56487 961b34963fa4
made N2M tactic more robust
src/HOL/Tools/BNF/bnf_fp_n2m.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 09 18:40:21 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 10 09:38:38 2014 +0200
@@ -373,7 +373,8 @@
 
     val co_recs = map (Morphism.term phi) raw_co_recs;
 
-    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms;
+    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms
+      |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
 
     val xtor_co_rec_thms =
       let
isabelle