Wed, 15 Dec 2010 11:26:28 +0100 | blanchet | added example to exercise higher-order reasoning with Sledgehammer and Metis | changeset | files |
Wed, 15 Dec 2010 11:26:28 +0100 | blanchet | added Sledgehammer support for higher-order propositional reasoning | changeset | files |
Wed, 15 Dec 2010 11:26:28 +0100 | blanchet | add Metis support for higher-order propositional reasoning | changeset | files |
Wed, 15 Dec 2010 11:26:28 +0100 | blanchet | implemented partially-typed "tags" type encoding | changeset | files |