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 work with theorems with multiple assumptions
authorblanchet
Sat, 21 Dec 2013 09:44:29 +0100
changeset 54843 7f30d569da08
parent 54842 a020f7d74fed
child 54844 630ba4d8a206
made tactic work with theorems with multiple assumptions
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	Sat Dec 21 09:44:28 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Sat Dec 21 09:44:29 2013 +0100
@@ -126,7 +126,11 @@
         NONE => (ms, f_ctrs)
       | SOME nchotomy =>
         (ms |> split_last ||> K [n - 1] |> op @,
-         f_ctrs |> split_last ||> (fn thm => [rulify_nchotomy n nchotomy RS thm]) |> op @));
+         f_ctrs
+         |> split_last
+         ||> unfold_thms ctxt @{thms atomize_conjL}
+         ||> (fn thm => [rulify_nchotomy n nchotomy RS thm])
+         |> op @));
   in
     EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
       ms' f_ctrs') THEN
isabelle