NTAC : int -> tactic -> tactic
STRUCTURE
Tactic
SYNOPSIS
Apply tactic a specified number of times.
DESCRIPTION
An invocation
NTAC n tac
applies the tactic
tac
exactly
n
times. If
n <= 0
then the goal is unchanged.
FAILURE
Fails if
tac
fails.
EXAMPLE
Suppose we have the following goal:
?- x = y
We apply a tactic for symmetry of equality 3 times:
NTAC 3 (PURE_ONCE_REWRITE_TAC [EQ_SYM_EQ])
and obtain
?- y = x
USES
Controlling iterated application tactics.
SEEALSO
PURE_ONCE_REWRITE_TAC
,
REPEAT
,
REPEATC
HOL
Kananaskis-14