src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
Tue, 31 Aug 2010 23:43:23 +0200 blanchet added "expect" feature of Nitpick to Sledgehammer, for regression testing
Tue, 31 Aug 2010 22:27:33 +0200 blanchet added "blocking" option to Sledgehammer to run in synchronous mode;
Thu, 26 Aug 2010 10:42:06 +0200 blanchet consider "locality" when assigning weights to facts
Wed, 25 Aug 2010 19:41:18 +0200 blanchet reorganize options regarding to the relevance threshold and decay
Wed, 25 Aug 2010 17:49:52 +0200 blanchet make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
Wed, 25 Aug 2010 09:32:43 +0200 blanchet get rid of "defs_relevant" feature;
Wed, 25 Aug 2010 09:02:07 +0200 blanchet renamed "relevance_convergence" to "relevance_decay"
Tue, 24 Aug 2010 19:19:28 +0200 blanchet compute names lazily;
Tue, 24 Aug 2010 18:03:43 +0200 blanchet clean handling of whether a fact is chained or not;
Tue, 24 Aug 2010 16:24:11 +0200 blanchet quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
Fri, 20 Aug 2010 16:44:48 +0200 blanchet unbreak "only" option of Sledgehammer
Fri, 20 Aug 2010 13:39:47 +0200 blanchet more fiddling with Sledgehammer's "add:" option
Wed, 18 Aug 2010 17:16:37 +0200 blanchet get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
Wed, 18 Aug 2010 17:09:05 +0200 blanchet added "max_relevant_per_iter" option to Sledgehammer
Wed, 18 Aug 2010 16:33:34 +0200 blanchet tuning
Tue, 17 Aug 2010 14:37:16 +0200 blanchet handle E's Skolem constants more gracefully
Mon, 09 Aug 2010 12:07:59 +0200 blanchet remove needless "open"
Mon, 09 Aug 2010 12:05:48 +0200 blanchet move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
less more (0) tip