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