| Mon, 19 Apr 2010 16:33:48 +0200 |
blanchet |
got rid of somewhat pointless "pairname" function in Sledgehammer
|
changeset |
files
|
| Mon, 19 Apr 2010 16:33:20 +0200 |
blanchet |
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
|
changeset |
files
|
| Mon, 19 Apr 2010 16:29:52 +0200 |
blanchet |
cosmetics
|
changeset |
files
|
| Mon, 19 Apr 2010 15:24:57 +0200 |
blanchet |
cosmetics
|
changeset |
files
|
| Mon, 19 Apr 2010 15:21:35 +0200 |
blanchet |
cosmetics
|
changeset |
files
|
| Mon, 19 Apr 2010 15:15:21 +0200 |
blanchet |
make Sledgehammer's minimizer also minimize Isar proofs
|
changeset |
files
|
| Mon, 19 Apr 2010 11:54:07 +0200 |
blanchet |
don't use readable names if proof reconstruction is needed, because it uses the structure of names
|
changeset |
files
|
| Mon, 19 Apr 2010 11:02:00 +0200 |
blanchet |
allow "_" in TPTP names in debug mode
|
changeset |
files
|
| Mon, 19 Apr 2010 10:45:08 +0200 |
blanchet |
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
|
changeset |
files
|
| Mon, 19 Apr 2010 10:15:02 +0200 |
blanchet |
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
|
changeset |
files
|
| Mon, 19 Apr 2010 09:53:31 +0200 |
blanchet |
get rid of "List.foldl" + add timestamp to SPASS
|
changeset |
files
|
| Tue, 20 Apr 2010 15:17:18 +0200 |
wenzelm |
less ambitious settings for cygwin-poly;
|
changeset |
files
|
| Tue, 20 Apr 2010 14:56:58 +0200 |
Cezary Kaliszyk |
respectfullness and preservation of map for identity quotients
|
changeset |
files
|
| Tue, 20 Apr 2010 14:56:20 +0200 |
Cezary Kaliszyk |
respectfullness and preservation of function composition
|
changeset |
files
|