src/HOL/Tools/Sledgehammer/metis_tactics.ML
Tue, 22 Jun 2010 14:28:22 +0200 blanchet removed Sledgehammer's support for the DFG syntax;
Mon, 21 Jun 2010 12:31:41 +0200 blanchet try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
Mon, 14 Jun 2010 20:16:36 +0200 blanchet A function called "untyped_aconv" shouldn't look at the bound names!
Mon, 14 Jun 2010 10:36:01 +0200 blanchet adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
Sat, 12 Jun 2010 11:11:07 +0200 blanchet "raise Fail" for internal errors + one new internal error (instead of "Match")
Fri, 11 Jun 2010 17:10:23 +0200 blanchet proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
Wed, 02 Jun 2010 12:28:42 +0200 blanchet give more helpful error message
Mon, 17 May 2010 12:15:37 +0200 blanchet fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
Mon, 17 May 2010 10:18:14 +0200 blanchet generate proper arity declarations for TFrees for SPASS's DFG format;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Fri, 14 May 2010 11:23:42 +0200 blanchet made Sledgehammer's full-typed proof reconstruction work for the first time;
Thu, 29 Apr 2010 10:25:26 +0200 blanchet use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
Mon, 26 Apr 2010 21:18:20 +0200 blanchet adapt code to reflect new signature of "neg_clausify"
Sat, 24 Apr 2010 16:05:42 +0200 blanchet better error reporting;
Mon, 19 Apr 2010 18:14:45 +0200 blanchet added warning about inconsistent context to Metis;
Fri, 16 Apr 2010 15:49:13 +0200 blanchet added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
Fri, 16 Apr 2010 14:48:34 +0200 blanchet store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
Thu, 15 Apr 2010 13:57:17 +0200 blanchet give more sensible names to "fol_type" constructors, as requested by a FIXME comment
Sun, 28 Mar 2010 16:59:06 +0200 wenzelm static defaults for configuration options;
Fri, 19 Mar 2010 13:02:18 +0100 blanchet more Sledgehammer refactoring
Wed, 17 Mar 2010 19:26:05 +0100 blanchet renamed Sledgehammer structures
Wed, 17 Mar 2010 18:16:31 +0100 blanchet move Sledgehammer files in a directory of their own
less more (0) tip