Q_TAC : (term -> tactic) -> term quotation -> tactic
STRUCTURE
SYNOPSIS
A tactical that parses in the context of a goal, a la the Q library.
DESCRIPTION
When applied to a term tactic T and a quotation q, the tactic Q_TAC T q first parses the quotation q in the context of the goal to yield the term tm, and then applies the tactic T tm to the goal.
FAILURE
The application of Q_TAC to a term tactic T and a quotation q never fails. The resulting composite tactic Q_TAC T q fails when applied to a goal if either q cannot be parsed, or T tm fails when applied to the goal.
COMMENTS
Useful for avoiding decorating terms with type abbreviations.
SEEALSO
HOL  Kananaskis-14