| #
621c1ebb |
|
13-Dec-2014 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
VALIDATE and VALIDATE_LT
If tac (ltac) is invalid due to proving theorems with extra assumptions,
VALIDATE tac and VALIDATE_LT ltac make the tactic valid by returning extra
subgoals to prove the extra assumptions
|