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 |