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
Mon, 17 Dec 2012 22:09:48 +0100 blanchet updated MaSh serialization number (to reflect new weights) file | diff | annotate
Mon, 17 Dec 2012 22:06:28 +0100 blanchet contain exponential explosion of term patterns file | diff | annotate
Mon, 17 Dec 2012 22:06:28 +0100 blanchet tuned weights -- keep same relative values, but use 1.0 as the least weight file | diff | annotate
Mon, 17 Dec 2012 22:06:28 +0100 blanchet really honor pattern depth, and use 2 by default file | diff | annotate
Sun, 16 Dec 2012 19:23:04 +0100 blanchet tuning file | diff | annotate
Sat, 15 Dec 2012 19:57:12 +0100 blanchet thread no timeout properly file | diff | annotate
Wed, 12 Dec 2012 02:47:45 +0100 blanchet merge aliased theorems in MaSh dependencies, modulo symmetry of equality file | diff | annotate
Wed, 12 Dec 2012 00:24:06 +0100 blanchet adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers) file | diff | annotate
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application; file | diff | annotate
Sat, 08 Dec 2012 00:48:51 +0100 blanchet don't have MaSh pretend it knows facts it doesn't know file | diff | annotate
Sat, 08 Dec 2012 00:48:50 +0100 blanchet fixed embarrassing off-by-one bug in MaSh's Mesh file | diff | annotate
Sat, 08 Dec 2012 00:48:50 +0100 blanchet tweak MaSh fudge factors file | diff | annotate
Sat, 08 Dec 2012 00:48:50 +0100 blanchet more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval" file | diff | annotate
Thu, 06 Dec 2012 17:48:04 +0100 blanchet use proper entry point for MaSh in test driver file | diff | annotate
Thu, 06 Dec 2012 15:54:17 +0100 blanchet parse more liberal MaSh suggestion syntax (for the eval driver) file | diff | annotate
Thu, 06 Dec 2012 11:25:10 +0100 blanchet tweaked MaSh proximity file | diff | annotate
Thu, 06 Dec 2012 11:25:10 +0100 blanchet reduce max number of dependencies for MaSh to get rid of junk file | diff | annotate
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
less more (0) -60 tip
isabelle