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:We apply a tactic for symmetry of equality 3 times:
?- x = y

and obtainNTAC 3 (PURE_ONCE_REWRITE_TAC [EQ_SYM_EQ])

?- y = x

- USES
- Controlling iterated application tactics.
- SEEALSO

HOL Kananaskis-14