Tue, 24 Aug 2010 18:03:43 +0200 |
blanchet |
clean handling of whether a fact is chained or not;
|
file |
diff |
annotate
|
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")
|
file |
diff |
annotate
|
Mon, 23 Aug 2010 14:54:17 +0200 |
blanchet |
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
|
file |
diff |
annotate
|
Fri, 20 Aug 2010 10:58:01 +0200 |
blanchet |
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
|
file |
diff |
annotate
|
Thu, 05 Aug 2010 12:40:12 +0200 |
blanchet |
fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
|
file |
diff |
annotate
|
Wed, 28 Jul 2010 18:54:18 +0200 |
blanchet |
minor refactoring
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 17:43:11 +0200 |
blanchet |
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
|
file |
diff |
annotate
|
Mon, 26 Jul 2010 17:03:21 +0200 |
blanchet |
generate full first-order formulas (FOF) in Sledgehammer
|
file |
diff |
annotate
|
Fri, 23 Jul 2010 21:29:29 +0200 |
blanchet |
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 16:27:53 +0200 |
blanchet |
exploit "Name.desymbolize" to remove some dependencies
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 14:28:22 +0200 |
blanchet |
removed Sledgehammer's support for the DFG syntax;
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 16:43:44 +0200 |
blanchet |
expect SPASS 3.7, and give a friendly warning if an older version is used
|
file |
diff |
annotate
|
Wed, 02 Jun 2010 15:18:48 +0200 |
blanchet |
honor "xsymbols"
|
file |
diff |
annotate
|
Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
Thu, 29 Apr 2010 01:17:14 +0200 |
blanchet |
expand combinators in Isar proofs constructed by Sledgehammer;
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 16:14:56 +0200 |
blanchet |
parentheses around nested cases
|
file |
diff |
annotate
|
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)
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 12:46:50 +0200 |
blanchet |
support Vampire definitions of constants as "let" constructs in Isar proofs
|
file |
diff |
annotate
|
Tue, 27 Apr 2010 16:00:20 +0200 |
blanchet |
fix types of "fix" variables to help proof reconstruction and aid readability
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 21:20:43 +0200 |
blanchet |
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
|
file |
diff |
annotate
|
Fri, 23 Apr 2010 19:12:49 +0200 |
blanchet |
remove some bloat
|
file |
diff |
annotate
|
Fri, 16 Apr 2010 16:13:49 +0200 |
blanchet |
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
|
file |
diff |
annotate
|
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)
|
file |
diff |
annotate
|
Fri, 16 Apr 2010 14:48:34 +0200 |
blanchet |
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
|
file |
diff |
annotate
|
Wed, 14 Apr 2010 18:23:51 +0200 |
blanchet |
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
|
file |
diff |
annotate
|
Mon, 29 Mar 2010 15:50:18 +0200 |
blanchet |
get rid of Polyhash, since it's no longer used
|
file |
diff |
annotate
|
Tue, 23 Mar 2010 11:39:21 +0100 |
blanchet |
added options to Sledgehammer;
|
file |
diff |
annotate
|