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
|
file |
diff |
annotate
|
Mon, 17 May 2010 10:18:14 +0200 |
blanchet |
generate proper arity declarations for TFrees for SPASS's DFG format;
|
file |
diff |
annotate
|
Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
Fri, 14 May 2010 11:23:42 +0200 |
blanchet |
made Sledgehammer's full-typed proof reconstruction work for the first time;
|
file |
diff |
annotate
|
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)
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 21:18:20 +0200 |
blanchet |
adapt code to reflect new signature of "neg_clausify"
|
file |
diff |
annotate
|
Sat, 24 Apr 2010 16:05:42 +0200 |
blanchet |
better error reporting;
|
file |
diff |
annotate
|
Mon, 19 Apr 2010 18:14:45 +0200 |
blanchet |
added warning about inconsistent context to Metis;
|
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
|
Thu, 15 Apr 2010 13:57:17 +0200 |
blanchet |
give more sensible names to "fol_type" constructors, as requested by a FIXME comment
|
file |
diff |
annotate
|
Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
Wed, 17 Mar 2010 19:26:05 +0100 |
blanchet |
renamed Sledgehammer structures
|
file |
diff |
annotate
|
Wed, 17 Mar 2010 18:16:31 +0100 |
blanchet |
move Sledgehammer files in a directory of their own
|
file |
diff |
annotate
| base
|