| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
more "metis" calls in example
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
minor textual improvement
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
wrap lambdas earlier, to get more control over beta/eta
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
move eta-contraction to before translation to Metis, to ensure everything stays in sync
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
avoid that var names get changed by resolution in Metis lambda-lifting
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
better threading of type encodings between Sledgehammer and "metis"
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
fixed bugs in lambda-lifting code -- ensure distinct names for variables
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
protect prefix against variant mutations
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
example cleanup
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
example cleanup
|
changeset |
files
|
| 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
|