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, 12 Nov 2012 11:32:22 +0100 blanchet thread context correctly when printing backquoted facts file | diff | annotate
Thu, 01 Nov 2012 15:00:48 +0100 blanchet made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory) file | diff | annotate
Mon, 06 Aug 2012 22:12:17 +0200 blanchet optimized saving file | diff | annotate
Fri, 03 Aug 2012 17:56:35 +0200 blanchet remember ATP flops to avoid repeating them too quickly file | diff | annotate
Fri, 03 Aug 2012 17:56:35 +0200 blanchet remember which MaSh proofs were found using ATPs file | diff | annotate
Fri, 03 Aug 2012 17:56:35 +0200 blanchet rule out same "technical" theories for MePo as for MaSh file | diff | annotate
Fri, 03 Aug 2012 17:56:35 +0200 blanchet crank up max number of dependencies file | diff | annotate
Fri, 03 Aug 2012 09:51:28 +0200 blanchet cleaner temporary file cleanup for MaSh, based on tried-and-trusted code file | diff | annotate
Thu, 26 Jul 2012 10:48:03 +0200 blanchet don't export technical theorems for MaSh file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet cap the number of facts returned by MaSh file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet remove MaSh junk associated with size functions file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet removed MaSh junk arising from primrec definitions file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet faster "save" operation file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet include unknown local facts in MaSh file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet ensure all calls to "mash" program are synchronous file | diff | annotate
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