• Jakob Botsch Nielsen's avatar
    Add contract_induction tactic · 6b7b7d05
    Jakob Botsch Nielsen authored
    This tactic applies contract_centric with evars and puts the "establish
    facts" obligation last. This allows the user to instantiate these during
    the proof of the property.
    6b7b7d05