1\DOC eta
2
3\TYPE {eta : tactic -> proof}
4
5\SYNOPSIS
6Applies a tactic to all goals, on which it succeeds, in the current goal list,
7replacing the list with the resulting subgoals.
8
9\DESCRIBE
10{eta tac} tries to apply {tac} to all the goals in the current goal list;
11replacing the goal list with the list of all the resulting subgoals.
12If it fails on a goal, it has no effect on that goal.
13It is an abbreviation for {expand_list (TRYALL tac)}.
14
15\USES
16For interactively constructing suitable compound tactics:
17in an interactive proof, the effect of {e (tac1 THEN TRY tac2)}
18can be obtained by {e tac1} and then {eta tac2}.
19
20\SEEALSO
21proofManagerLib.expand_list,
22proofManagerLib.elt,
23Tactical.TRYALL,
24Tactical.TRY,
25proofManagerLib.eall,
26proofManagerLib.set_goal.
27
28\ENDDOC
29