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.
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
authorblanchet
Wed, 03 Sep 2014 22:47:05 +0200
changeset 58170 d84bab7ed89e
parent 58169 68a2cf857df1
child 58171 5777ec326822
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
src/HOL/Library/bnf_lfp_countable.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
@@ -160,7 +160,7 @@
       val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
 
       val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
-      val goal = HOLogic.mk_Trueprop (Balanced_Tree.make HOLogic.mk_conj conjuncts);
+      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
     in
       Goal.prove ctxt [] [] goal (fn {context = ctxt, prems = _} =>
         mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
isabelle