Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
Mon, 23 Jul 2012 15:32:30 +0200 blanchet don't relearn old facts in Isar mode file | diff | annotate
Fri, 20 Jul 2012 22:43:51 +0200 blanchet tune Mesh filter file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet faster maximal node computation file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet honor suggested MaSh weights file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet relearn ATP proofs file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet don't store fresh names in fact graph, since these cannot be the parents of any other facts file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet cached ancestor computation file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet minimal maxes + tuning file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn from SMT proofs when they can be minimized by Metis file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet clean up interesting constants a bit file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet name tuning file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learning should honor the fact override and the chained facts file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet added "learn_from_atp" command to MaSh, for patient users file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet add versioning to MaSh state + cleanup dead code file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet eliminated special handling of init case, now that "mash.py" has been optimized to handle sequences of add gracefully file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet added locality as a MaSh feature file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn command in MaSh file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet added possibility of running external MaSh commands asynchronously file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML structures file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML files file | diff | annotate | base
less more (0) tip
isabelle