partial evaluation of locale facts leads to static scoping of rule attributes;

tuned message;

gave SML/NJ a chance

more robust options

adding another example for lifting definitions

improving header

more "metis" calls in example

be more silent when auto minimizing

less offensive terminology

more "metis" calls in example

minor textual improvement

pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones

wrap lambdas earlier, to get more control over beta/eta

move eta-contraction to before translation to Metis, to ensure everything stays in sync

avoid that var names get changed by resolution in Metis lambda-lifting

better threading of type encodings between Sledgehammer and "metis"

fixed bugs in lambda-lifting code -- ensure distinct names for variables

protect prefix against variant mutations

example cleanup

example cleanup

don't propagate user-set "type_enc" or "lam_trans" to Metis calls

don't needlessly pass "lam_lifted" option to "metis" call for SMT proof

avoid spurious messages in "lam_lifting" mode

eta-contract to avoid needless "lambda" wrappers

quiet down SMT

more aggressive lambda hiding (if we anyway need to pass an option to Metis)

updated Sledgehammer docs

don't pass "lam_lifted" option to "metis" unless there's a good reason