2011-05-31 | blanchet | added new metis mode, with no implementation yet | changeset | files |
2011-05-31 | blanchet | tuning | changeset | files |
2011-05-31 | blanchet | first step in sharing more code between ATP and Metis translation | changeset | files |
2011-05-31 | krauss | more precise authorship, reflecting my own ignorance and hg annotate | changeset | files |
2011-05-31 | krauss | generate raw induction rule as instance of generic rule with careful treatment of currying | changeset | files |
2011-05-31 | krauss | generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type | changeset | files |
2011-05-31 | krauss | admissibility on option type | changeset | files |
Loading... |