src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
Wed, 02 Jun 2010 15:18:48 +0200 blanchet honor "xsymbols"
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Thu, 29 Apr 2010 01:17:14 +0200 blanchet expand combinators in Isar proofs constructed by Sledgehammer;
Wed, 28 Apr 2010 16:14:56 +0200 blanchet parentheses around nested cases
Wed, 28 Apr 2010 15:34:55 +0200 blanchet unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
Wed, 28 Apr 2010 12:46:50 +0200 blanchet support Vampire definitions of constants as "let" constructs in Isar proofs
Tue, 27 Apr 2010 16:00:20 +0200 blanchet fix types of "fix" variables to help proof reconstruction and aid readability
Mon, 26 Apr 2010 21:20:43 +0200 blanchet introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
Fri, 23 Apr 2010 19:12:49 +0200 blanchet remove some bloat
Fri, 16 Apr 2010 16:13:49 +0200 blanchet Sledgehammer: the empty set of fact () should mean nothing, not unchanged
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
Wed, 14 Apr 2010 18:23:51 +0200 blanchet make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
Mon, 29 Mar 2010 15:50:18 +0200 blanchet get rid of Polyhash, since it's no longer used
Tue, 23 Mar 2010 11:39:21 +0100 blanchet added options to Sledgehammer;
less more (0) tip