Fri, 18 Nov 2011 11:47:12 +0100 | blanchet | don't propagate user-set "type_enc" or "lam_trans" to Metis calls | changeset | files |
Fri, 18 Nov 2011 11:47:12 +0100 | blanchet | don't needlessly pass "lam_lifted" option to "metis" call for SMT proof | changeset | files |
Fri, 18 Nov 2011 11:47:12 +0100 | blanchet | avoid spurious messages in "lam_lifting" mode | changeset | files |
Fri, 18 Nov 2011 11:47:12 +0100 | blanchet | eta-contract to avoid needless "lambda" wrappers | changeset | files |
Fri, 18 Nov 2011 11:47:12 +0100 | blanchet | quiet down SMT | changeset | files |
Fri, 18 Nov 2011 11:47:12 +0100 | blanchet | more aggressive lambda hiding (if we anyway need to pass an option to Metis) | changeset | files |
Fri, 18 Nov 2011 11:47:12 +0100 | blanchet | updated Sledgehammer docs | changeset | files |