REPEAT_GTCL : thm_tactical -> thm_tactical
Applies a theorem-tactical until it fails when applied to a goal.
When applied to a theorem-tactical, a theorem-tactic, a theorem and a goal:
REPEAT_GTCL repeatedly modifies the theorem according to
ttl till the result of handing it to ttac and applying it to the goal
fails (this may be no times at all).
REPEAT_GTCL ttl ttac th goal
- FAILURE CONDITIONS
Fails iff the theorem-tactic fails immediately when applied to the theorem
and the goal.
The following tactic matches th's antecedents against the assumptions
of the goal until it can do so no longer, then puts the resolvents
onto the assumption list:
REPEAT_GTCL IMP_RES_THEN ASSUME_TAC th
- SEE ALSO