• Robbert Krebbers's avatar
    More introduction patterns. · 4d8c4ac8
    Robbert Krebbers authored
    Also make those for introduction and elimination more symmetric:
    
      !%   pure introduction         %        pure elimination
      !#   always introduction       #        always elimination
      !>   later introduction        > pat    timeless later elimination
      !==> view shift introduction   ==> pat  view shift elimination
    4d8c4ac8
ProofMode.md 8.94 KB