• Jacques-Henri Jourdan's avatar
    Remove notations for bi_bare and bi_persistently. · a38db108
    Jacques-Henri Jourdan authored
    (□ P) now means (bi_bare (bi_persistently P)).
    
    This is motivated by the fact that these two modalities are rarely
    used separately.
    
    In the case of an affine BI, we keep the □ notation. This means that a
    bi_bare is inserted each time we use □. Hence, a few adaptations need
    to be done in the proof mode class instances.
    a38db108
derived.v 4.68 KB