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.
do a second phase of proof compression after minimization
authorblanchet
Tue, 04 Feb 2014 23:11:18 +0100
changeset 55327 3c7f3122ccdc
parent 55326 cc627ced3874
child 55328 0e17e92248ac
do a second phase of proof compression after minimization
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 23:11:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -322,6 +322,9 @@
                (keep_fastest_method_of_isar_step (!preplay_data)
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
+          |> minimize
+               ? (compress_isar_proof ctxt compress_isar preplay_data
+                  #> tap (trace_isar_proof "Compressed again"))
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof
isabelle