Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
less offensive terminology
|
changeset |
files
|
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
|