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.
normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
authorwenzelm
Tue, 14 Jul 2015 11:29:43 +0200
changeset 60722 a8babbb6d5ea
parent 60719 b6713e04889e
child 60723 757cad5a3fe9
normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
src/Pure/goal.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/goal.ML	Mon Jul 13 19:25:58 2015 +0200
+++ b/src/Pure/goal.ML	Tue Jul 14 11:29:43 2015 +0200
@@ -230,7 +230,9 @@
             result)
           (Thm.term_of stmt);
   in
-    Conjunction.elim_balanced (length props) res
+    res
+    |> length props > 1 ? Thm.norm_proof
+    |> Conjunction.elim_balanced (length props)
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt
     |> map Drule.zero_var_indexes
isabelle