| Fri, 04 Jun 2010 16:54:10 +0200 |
blanchet |
recongize one more outcome string for "remote_vampire"
|
file |
diff |
annotate
|
| Fri, 28 May 2010 13:49:21 +0200 |
blanchet |
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
|
file |
diff |
annotate
|
| Mon, 17 May 2010 10:16:54 +0200 |
blanchet |
identify common SPASS error more clearly
|
file |
diff |
annotate
|
| Fri, 14 May 2010 22:29:50 +0200 |
blanchet |
renamed options
|
file |
diff |
annotate
|
| Fri, 14 May 2010 16:15:10 +0200 |
blanchet |
renamed two Sledgehammer options
|
file |
diff |
annotate
|
| Fri, 14 May 2010 15:26:26 +0200 |
blanchet |
query _HOME environment variables at run-time, not at build-time
|
file |
diff |
annotate
|
| Fri, 14 May 2010 11:24:14 +0200 |
blanchet |
pass "full_type" argument to proof reconstruction
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 19:08:02 +0200 |
blanchet |
in "overlord" mode: ignore problem prefix specified in the .thy file
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 22:00:48 +0200 |
blanchet |
back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 17:56:07 +0200 |
blanchet |
properly extract SPASS proof
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 17:47:30 +0200 |
blanchet |
try out Vampire 11 and parse its output correctly;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:32:45 +0200 |
blanchet |
removed "sorts" option, continued
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 18:58:05 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 11:24:47 +0200 |
blanchet |
remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 21:17:41 +0200 |
blanchet |
rename options and keep track of conjecture shape (to facilitate proof reconstruction)
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 11:38:46 +0200 |
blanchet |
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 19:36:49 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 18:11:41 +0200 |
blanchet |
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
|
file |
diff |
annotate
| base
|