Mon, 20 May 2013 12:35:29 +0200 | blanchet | freeze types in Sledgehammer goal, not just terms | changeset | files |
Mon, 20 May 2013 11:49:56 +0200 | blanchet | generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue) | changeset | files |