src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
Mon, 17 Dec 2012 22:09:48 +0100 blanchet updated MaSh serialization number (to reflect new weights)
Mon, 17 Dec 2012 22:06:28 +0100 blanchet contain exponential explosion of term patterns
Mon, 17 Dec 2012 22:06:28 +0100 blanchet tuned weights -- keep same relative values, but use 1.0 as the least weight
Mon, 17 Dec 2012 22:06:28 +0100 blanchet really honor pattern depth, and use 2 by default
Sun, 16 Dec 2012 19:23:04 +0100 blanchet tuning
Sat, 15 Dec 2012 19:57:12 +0100 blanchet thread no timeout properly
Wed, 12 Dec 2012 02:47:45 +0100 blanchet merge aliased theorems in MaSh dependencies, modulo symmetry of equality
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)
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
Sat, 08 Dec 2012 00:48:51 +0100 blanchet don't have MaSh pretend it knows facts it doesn't know
Sat, 08 Dec 2012 00:48:50 +0100 blanchet fixed embarrassing off-by-one bug in MaSh's Mesh
Sat, 08 Dec 2012 00:48:50 +0100 blanchet tweak MaSh fudge factors
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"
Thu, 06 Dec 2012 17:48:04 +0100 blanchet use proper entry point for MaSh in test driver
Thu, 06 Dec 2012 15:54:17 +0100 blanchet parse more liberal MaSh suggestion syntax (for the eval driver)
Thu, 06 Dec 2012 11:25:10 +0100 blanchet tweaked MaSh proximity
Thu, 06 Dec 2012 11:25:10 +0100 blanchet reduce max number of dependencies for MaSh to get rid of junk
Thu, 06 Dec 2012 11:25:10 +0100 blanchet more feature tweaks
Thu, 06 Dec 2012 11:25:10 +0100 blanchet prioritize chained facts
Thu, 06 Dec 2012 11:25:10 +0100 blanchet more MaSh feature tweaking
Thu, 06 Dec 2012 11:25:10 +0100 blanchet record free variables as a MaSh feature
Thu, 06 Dec 2012 11:25:10 +0100 blanchet expand type classes into their ancestors for MaSh
Thu, 06 Dec 2012 11:25:10 +0100 blanchet tweaked MaSh features, based on comments by Josef Urban
Thu, 06 Dec 2012 11:25:10 +0100 blanchet increase weight of local facts again (MaSh)
Thu, 06 Dec 2012 11:25:10 +0100 blanchet simplify code now that "mash.py" supports weights
Wed, 05 Dec 2012 13:25:06 +0100 blanchet take proximity into account for MaSh + fix a debilitating bug in feature generation
Wed, 05 Dec 2012 13:25:06 +0100 blanchet tuning
Wed, 05 Dec 2012 10:35:58 +0100 blanchet tweaked order of theorems to avoid forward dependencies (MaSh)
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
Tue, 04 Dec 2012 23:19:03 +0100 blanchet added feature weights in MaSh
Tue, 04 Dec 2012 23:19:02 +0100 blanchet promote local facts using a hack (for MaSh)
Tue, 04 Dec 2012 19:10:14 +0100 blanchet turned off noisy MaSh features
Tue, 04 Dec 2012 10:02:51 +0100 blanchet simplify MaSh term patterns + add missing global facts if there aren't too many
Tue, 04 Dec 2012 00:37:11 +0100 blanchet MaSh improvements: deeper patterns + more respect for chained facts
Mon, 03 Dec 2012 23:43:53 +0100 blanchet tuned names
Mon, 03 Dec 2012 20:55:34 +0100 blanchet proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
Mon, 03 Dec 2012 13:24:55 +0100 blanchet robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
Sat, 01 Dec 2012 23:55:39 +0100 blanchet tuned order of functions
Sat, 01 Dec 2012 23:55:38 +0100 blanchet proper quoting of paths in MaSh
Mon, 26 Nov 2012 15:31:03 +0100 blanchet simplify code slightly
Mon, 26 Nov 2012 12:04:32 +0100 blanchet moved MaSh's Python code into Isabelle
Thu, 22 Nov 2012 13:21:02 +0100 wenzelm more abstract Sendback operations, with explicit id/exec_id properties;
Mon, 12 Nov 2012 11:32:22 +0100 blanchet thread context correctly when printing backquoted facts
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)
Mon, 06 Aug 2012 22:12:17 +0200 blanchet optimized saving
Fri, 03 Aug 2012 17:56:35 +0200 blanchet remember ATP flops to avoid repeating them too quickly
Fri, 03 Aug 2012 17:56:35 +0200 blanchet remember which MaSh proofs were found using ATPs
Fri, 03 Aug 2012 17:56:35 +0200 blanchet rule out same "technical" theories for MePo as for MaSh
Fri, 03 Aug 2012 17:56:35 +0200 blanchet crank up max number of dependencies
Fri, 03 Aug 2012 09:51:28 +0200 blanchet cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
Thu, 26 Jul 2012 10:48:03 +0200 blanchet don't export technical theorems for MaSh
Mon, 23 Jul 2012 15:32:30 +0200 blanchet cap the number of facts returned by MaSh
Mon, 23 Jul 2012 15:32:30 +0200 blanchet remove MaSh junk associated with size functions
Mon, 23 Jul 2012 15:32:30 +0200 blanchet identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway
Mon, 23 Jul 2012 15:32:30 +0200 blanchet removed MaSh junk arising from primrec definitions
Mon, 23 Jul 2012 15:32:30 +0200 blanchet distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
Mon, 23 Jul 2012 15:32:30 +0200 blanchet faster "save" operation
Mon, 23 Jul 2012 15:32:30 +0200 blanchet include unknown local facts in MaSh
Mon, 23 Jul 2012 15:32:30 +0200 blanchet ensure all calls to "mash" program are synchronous
Mon, 23 Jul 2012 15:32:30 +0200 blanchet don't relearn old facts in Isar mode
less more (0) -60 tip