1. 15 Mar, 2016 2 commits
  2. 20 Mar, 2015 1 commit
  3. 19 Mar, 2015 1 commit
  4. 22 Sep, 2014 1 commit
  5. 18 Sep, 2014 2 commits
  6. 17 Sep, 2014 1 commit
    • Léon Gondelman's avatar
      New transformations induction_pr and inversion_pr. · 8388828a
      Léon Gondelman authored
      Induction_pr performs induction on the leftmost application
      of some inductive predicate in the goal.
      
      This can be overriden by attaching the label "induction"
      on such an application. In this case, any unlabeled application
      will be ignored.
      
      Inversion_pr works similarly, excepted that it does not generate
      inductive hypotheses, but simply inverses inductive predicate.
      In this case, the label "inversion" will be used.
      8388828a