| Thu, 16 Sep 2010 14:26:09 +0200 |
blanchet |
merged
|
changeset |
files
|
| Thu, 16 Sep 2010 14:24:48 +0200 |
blanchet |
avoid code duplication
|
changeset |
files
|
| Thu, 16 Sep 2010 14:24:03 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 16 Sep 2010 13:52:17 +0200 |
blanchet |
merge constructors
|
changeset |
files
|
| Thu, 16 Sep 2010 13:44:41 +0200 |
blanchet |
factor out the inverse of "nice_atp_problem"
|
changeset |
files
|
| Thu, 16 Sep 2010 11:59:45 +0200 |
blanchet |
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
|
changeset |
files
|
| Thu, 16 Sep 2010 11:12:08 +0200 |
blanchet |
factored out TSTP/SPASS/Vampire proof parsing;
|
changeset |
files
|
| Thu, 16 Sep 2010 09:59:32 +0200 |
blanchet |
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
|
changeset |
files
|
| Thu, 16 Sep 2010 08:29:50 +0200 |
blanchet |
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
|
changeset |
files
|
| Thu, 16 Sep 2010 08:27:10 +0200 |
blanchet |
regenerated "metis.ML"
|
changeset |
files
|
| Thu, 16 Sep 2010 08:02:32 +0200 |
blanchet |
streamlined "make_metis"
|
changeset |
files
|
| Thu, 16 Sep 2010 07:54:18 +0200 |
blanchet |
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
|
changeset |
files
|