Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
Thu, 06 Dec 2012 11:25:10 +0100 blanchet more feature tweaks file | diff | annotate
Thu, 06 Dec 2012 11:25:10 +0100 blanchet prioritize chained facts file | diff | annotate
Thu, 06 Dec 2012 11:25:10 +0100 blanchet more MaSh feature tweaking file | diff | annotate
Thu, 06 Dec 2012 11:25:10 +0100 blanchet record free variables as a MaSh feature file | diff | annotate
Thu, 06 Dec 2012 11:25:10 +0100 blanchet expand type classes into their ancestors for MaSh file | diff | annotate
Thu, 06 Dec 2012 11:25:10 +0100 blanchet tweaked MaSh features, based on comments by Josef Urban file | diff | annotate
Thu, 06 Dec 2012 11:25:10 +0100 blanchet increase weight of local facts again (MaSh) file | diff | annotate
Thu, 06 Dec 2012 11:25:10 +0100 blanchet simplify code now that "mash.py" supports weights file | diff | annotate
Wed, 05 Dec 2012 13:25:06 +0100 blanchet take proximity into account for MaSh + fix a debilitating bug in feature generation file | diff | annotate
Wed, 05 Dec 2012 13:25:06 +0100 blanchet tuning file | diff | annotate
Wed, 05 Dec 2012 10:35:58 +0100 blanchet tweaked order of theorems to avoid forward dependencies (MaSh) file | diff | annotate
Tue, 04 Dec 2012 23:43:24 +0100 blanchet more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions file | diff | annotate
Tue, 04 Dec 2012 23:19:03 +0100 blanchet added feature weights in MaSh file | diff | annotate
Tue, 04 Dec 2012 23:19:02 +0100 blanchet promote local facts using a hack (for MaSh) file | diff | annotate
Tue, 04 Dec 2012 19:10:14 +0100 blanchet turned off noisy MaSh features file | diff | annotate
Tue, 04 Dec 2012 10:02:51 +0100 blanchet simplify MaSh term patterns + add missing global facts if there aren't too many file | diff | annotate
Tue, 04 Dec 2012 00:37:11 +0100 blanchet MaSh improvements: deeper patterns + more respect for chained facts file | diff | annotate
Mon, 03 Dec 2012 23:43:53 +0100 blanchet tuned names file | diff | annotate
Mon, 03 Dec 2012 20:55:34 +0100 blanchet proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e) file | diff | annotate
Mon, 03 Dec 2012 13:24:55 +0100 blanchet robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer file | diff | annotate
Sat, 01 Dec 2012 23:55:39 +0100 blanchet tuned order of functions file | diff | annotate
Sat, 01 Dec 2012 23:55:38 +0100 blanchet proper quoting of paths in MaSh file | diff | annotate
Mon, 26 Nov 2012 15:31:03 +0100 blanchet simplify code slightly file | diff | annotate
Mon, 26 Nov 2012 12:04:32 +0100 blanchet moved MaSh's Python code into Isabelle file | diff | annotate
Thu, 22 Nov 2012 13:21:02 +0100 wenzelm more abstract Sendback operations, with explicit id/exec_id properties; file | diff | annotate
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
less more (0) -60 tip
isabelle