• Robbert Krebbers's avatar
    Allow `iSpecialize` to be nested. · c6af67f9
    Robbert Krebbers authored
    It now supports the specialization pattern `(H spat1 .. spatn)`, which first
    recursively specializes the hypothesis `H` using the specialization patterns
    `spat1 .. spatn`.
    c6af67f9
ProofMode.md 15.4 KB