Applies a theorem-tactical until it fails when applied to a goal.
DESCRIPTION
When applied to a theorem-tactical, a theorem-tactic, a theorem and a goal:
REPEAT_GTCL ttl ttac th 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).
FAILURE
Fails iff the theorem-tactic fails immediately when applied to the theorem
and the goal.
EXAMPLE
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: