src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
2013-01-31 blanchet 2013-01-31 adapted to new MaSh interface
2013-01-19 blanchet 2013-01-19 tuning
2013-01-18 blanchet 2013-01-18 tuning
2013-01-18 blanchet 2013-01-18 optimization -- evaluate conversion to table only once
2013-01-17 blanchet 2013-01-17 use correct weights in MeSh driver
2013-01-17 blanchet 2013-01-17 evaluate more cases (cf. paper)
2013-01-17 blanchet 2013-01-17 updated MaSh
2013-01-14 blanchet 2013-01-14 adjust weights -- sorts are prolific, so tone them down even more
2013-01-13 blanchet 2013-01-13 don't learn theories -- this option is very slow and not very helpful
2013-01-13 blanchet 2013-01-13 honor unknown chained in MaSh and a few other tweaks
2013-01-13 blanchet 2013-01-13 remove obsolete MaSh files
2013-01-13 blanchet 2013-01-13 cleaned up hint handling
2013-01-13 blanchet 2013-01-13 better handlig of built-ins -- at the top-level, not in subterms
2013-01-12 blanchet 2013-01-12 honor filtering out of arguments for built-in constants (e.g. representation of numerals)
2013-01-12 blanchet 2013-01-12 new version of MaSh Python component
2013-01-11 blanchet 2013-01-11 don't learn from the proof of "psimps" etc.
2013-01-11 blanchet 2013-01-11 updated MaSh Python component
2013-01-11 blanchet 2013-01-11 start using MaSh hints
2013-01-11 blanchet 2013-01-11 always compare theorem using the same, weaker function
2013-01-10 blanchet 2013-01-10 export MeSh data as well
2013-01-06 blanchet 2013-01-06 get rid of spurious "Isar" proofs
2013-01-06 blanchet 2013-01-06 also generate queries for goals with too many Isar dependencies
2013-01-05 blanchet 2013-01-05 tuned message
2013-01-05 blanchet 2013-01-05 tap after, not before command invocation
2013-01-04 blanchet 2013-01-04 refined class handling, to prevent cycles in fact graph
2013-01-04 blanchet 2013-01-04 tweaked nicknames
2013-01-04 blanchet 2013-01-04 speed up generation of local theorem nicknames
2013-01-04 blanchet 2013-01-04 tweaked fudge factor
2013-01-02 blanchet 2013-01-02 tuning
2012-12-28 blanchet 2012-12-28 tuned ML function name
2012-12-28 blanchet 2012-12-28 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
2012-12-28 blanchet 2012-12-28 tuned ML function names
2012-12-27 blanchet 2012-12-27 improved thm order hack, in case the default names are overridden
2012-12-27 blanchet 2012-12-27 enable theory learning in MaSh
2012-12-21 blanchet 2012-12-21 name tuning
2012-12-20 blanchet 2012-12-20 better weight functions for MePo/MaSh etc.
2012-12-17 blanchet 2012-12-17 updated MaSh serialization number (to reflect new weights)
2012-12-17 blanchet 2012-12-17 contain exponential explosion of term patterns
2012-12-17 blanchet 2012-12-17 tuned weights -- keep same relative values, but use 1.0 as the least weight
2012-12-17 blanchet 2012-12-17 really honor pattern depth, and use 2 by default
2012-12-16 blanchet 2012-12-16 tuning
2012-12-15 blanchet 2012-12-15 thread no timeout properly
2012-12-12 blanchet 2012-12-12 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
2012-12-12 blanchet 2012-12-12 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
2012-12-10 wenzelm 2012-12-10 generalized notion of active area, where sendback is just one application; some support for graphview via active area;
2012-12-08 blanchet 2012-12-08 don't have MaSh pretend it knows facts it doesn't know
2012-12-08 blanchet 2012-12-08 fixed embarrassing off-by-one bug in MaSh's Mesh
2012-12-08 blanchet 2012-12-08 tweak MaSh fudge factors
2012-12-08 blanchet 2012-12-08 more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
2012-12-06 blanchet 2012-12-06 use proper entry point for MaSh in test driver
2012-12-06 blanchet 2012-12-06 parse more liberal MaSh suggestion syntax (for the eval driver)
2012-12-06 blanchet 2012-12-06 tweaked MaSh proximity
2012-12-06 blanchet 2012-12-06 reduce max number of dependencies for MaSh to get rid of junk
2012-12-06 blanchet 2012-12-06 more feature tweaks
2012-12-06 blanchet 2012-12-06 prioritize chained facts
2012-12-06 blanchet 2012-12-06 more MaSh feature tweaking
2012-12-06 blanchet 2012-12-06 record free variables as a MaSh feature
2012-12-06 blanchet 2012-12-06 expand type classes into their ancestors for MaSh
2012-12-06 blanchet 2012-12-06 tweaked MaSh features, based on comments by Josef Urban
2012-12-06 blanchet 2012-12-06 increase weight of local facts again (MaSh)