`REPEAT : tactic -> tactic`

SYNOPSIS
Repeatedly applies a tactic until it fails.

DESCRIPTION
The tactic REPEAT t is a tactic which applies t to a goal, and while it succeeds, continues applying it to all subgoals generated.

FAILURE CONDITIONS
The application of REPEAT to a tactic never fails, and neither does the composite tactic, even if the basic tactic fails immediately, unless it raises an exception other that Failure ....

EXAMPLE
If we start with a goal having many universal quantifiers:
```  # g `!w x y z. w < z /\ x < y ==> w * x + 1 <= y * z`;;
```
then GEN_TAC will strip them off one at a time:
```  # e GEN_TAC;;
val it : goalstack = 1 subgoal (1 total)

`!x y z. w < z /\ x < y ==> w * x + 1 <= y * z`
```
and REPEAT GEN_TAC will strip them off as far as possible:
```  # e(REPEAT GEN_TAC);;
val it : goalstack = 1 subgoal (1 total)

`w < z /\ x < y ==> w * x + 1 <= y * z`
```
Similarly, REPEAT COND_CASES_TAC will eliminate all free conditionals in the goal instead of just one.