| 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 |