• Robbert Krebbers's avatar
    Remove Existing Class Is_true. · 82138115
    Robbert Krebbers authored
    Having Is_true as a type class caused problems with rewrite: when the
    rewrited lemma has a premise of the shape Is_true, the rewrite tactic
    will complain that it cannot find a type class instance, instead
    of generating a goal for that premise.
    82138115
base.v 41.3 KB