Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

  • 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 58.9 KB