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.
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
authorwenzelm
Fri, 23 Dec 2005 15:16:44 +0100
changeset 18496 ef36f9be255e
parent 18495 1b96c8671162
child 18497 7569674d7bb1
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
src/Provers/induct_method.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/induct_method.ML	Fri Dec 23 14:33:28 2005 +0100
+++ b/src/Provers/induct_method.ML	Fri Dec 23 15:16:44 2005 +0100
@@ -417,8 +417,8 @@
       ruleq
       |> Seq.maps (RuleCases.consume (List.concat defs) facts)
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
-        (CONJUNCTS (length concls) (ALLGOALS (fn j =>
-          (CONJUNCTS ~1 (ALLGOALS
+        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
+          (CONJUNCTS (ALLGOALS
             (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
               THEN' fix_tac defs_ctxt
                 (nth concls (j - 1) + more_consumes)
isabelle