| Wed, 20 Feb 2013 10:45:23 +0100 | blanchet | optimize Isar output some more | changeset | files |
| Wed, 20 Feb 2013 10:45:01 +0100 | blanchet | turn off more evil Vampire options to facilitate Isar proof generation | changeset | files |
| Wed, 20 Feb 2013 09:58:28 +0100 | blanchet | fixed typo in option name | changeset | files |
| Wed, 20 Feb 2013 08:56:34 +0100 | blanchet | tuning | changeset | files |
| Wed, 20 Feb 2013 08:44:24 +0100 | blanchet | use new skolemizer only if some skolems have two or more arguments -- otherwise the old skolemizer cannot get the arg order wrong | changeset | files |
| Wed, 20 Feb 2013 08:44:24 +0100 | blanchet | slacker comparison for Skolems, to avoid trivial equations | changeset | files |
| Wed, 20 Feb 2013 08:44:24 +0100 | blanchet | auto-minimizer should respect "isar_proofs = true" | changeset | files |
| Wed, 20 Feb 2013 08:44:24 +0100 | blanchet | made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired | changeset | files |