src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
Sat, 19 Jan 2013 17:42:12 +0100 blanchet tuning
Fri, 18 Jan 2013 16:06:45 +0100 blanchet tuning
Fri, 18 Jan 2013 00:18:11 +0100 blanchet optimization -- evaluate conversion to table only once
Thu, 17 Jan 2013 23:29:22 +0100 blanchet use correct weights in MeSh driver
Thu, 17 Jan 2013 18:43:59 +0100 blanchet evaluate more cases (cf. paper)
Thu, 17 Jan 2013 17:55:03 +0100 blanchet updated MaSh
Mon, 14 Jan 2013 09:59:50 +0100 blanchet adjust weights -- sorts are prolific, so tone them down even more
Sun, 13 Jan 2013 22:17:00 +0100 blanchet don't learn theories -- this option is very slow and not very helpful
Sun, 13 Jan 2013 20:57:48 +0100 blanchet honor unknown chained in MaSh and a few other tweaks
Sun, 13 Jan 2013 15:04:55 +0100 blanchet remove obsolete MaSh files
Sun, 13 Jan 2013 12:15:44 +0100 blanchet cleaned up hint handling
Sun, 13 Jan 2013 12:15:43 +0100 blanchet better handlig of built-ins -- at the top-level, not in subterms
Sat, 12 Jan 2013 16:49:40 +0100 blanchet honor filtering out of arguments for built-in constants (e.g. representation of numerals)
Sat, 12 Jan 2013 16:49:39 +0100 blanchet new version of MaSh Python component
Fri, 11 Jan 2013 16:30:56 +0100 blanchet don't learn from the proof of "psimps" etc.
Fri, 11 Jan 2013 16:30:56 +0100 blanchet updated MaSh Python component
Fri, 11 Jan 2013 16:30:56 +0100 blanchet start using MaSh hints
Fri, 11 Jan 2013 16:30:56 +0100 blanchet always compare theorem using the same, weaker function
Thu, 10 Jan 2013 23:34:19 +0100 blanchet export MeSh data as well
Sun, 06 Jan 2013 17:38:29 +0100 blanchet get rid of spurious "Isar" proofs
Sun, 06 Jan 2013 17:38:29 +0100 blanchet also generate queries for goals with too many Isar dependencies
Sat, 05 Jan 2013 22:31:33 +0100 blanchet tuned message
Sat, 05 Jan 2013 22:31:32 +0100 blanchet tap after, not before command invocation
Fri, 04 Jan 2013 21:56:20 +0100 blanchet refined class handling, to prevent cycles in fact graph
Fri, 04 Jan 2013 21:56:19 +0100 blanchet tweaked nicknames
Fri, 04 Jan 2013 19:00:49 +0100 blanchet speed up generation of local theorem nicknames
Fri, 04 Jan 2013 19:00:49 +0100 blanchet tweaked fudge factor
Wed, 02 Jan 2013 10:41:53 +0100 blanchet tuning
Fri, 28 Dec 2012 23:31:51 +0100 blanchet tuned ML function name
Fri, 28 Dec 2012 21:03:39 +0100 blanchet slightly more elegant naming convention (to keep low-level and high-level APIs separated)
Fri, 28 Dec 2012 14:13:39 +0100 blanchet tuned ML function names
Thu, 27 Dec 2012 16:49:12 +0100 blanchet improved thm order hack, in case the default names are overridden
Thu, 27 Dec 2012 15:46:27 +0100 blanchet enable theory learning in MaSh
Fri, 21 Dec 2012 14:35:29 +0100 blanchet name tuning
Thu, 20 Dec 2012 15:51:27 +0100 blanchet better weight functions for MePo/MaSh etc.
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
less more (0) -100 -60 tip