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