-
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
It now supports the specialization pattern `(H spat1 .. spatn)`, which first recursively specializes the hypothesis `H` using the specialization patterns `spat1 .. spatn`.