NTAC : int -> tactic -> tactic
STRUCTURE
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
HOL  Kananaskis-13