HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Published 20 hours ago • verified publisher icon HOL-Theorem-Prover

Add spec form to cover both `INST` and `SPEC` of theorems

Open mn200 opened this issue 3 months ago • 0 comments

It should be possible to specialise variables without knowing where in a quantification block they are, and if free, the effect can be as of INST.

mn200 avatar Apr 11 '24 04:04 mn200