eta : tactic -> proof
STRUCTURE
SYNOPSIS
Applies a tactic to all goals, on which it succeeds, in the current goal list, replacing the list with the resulting subgoals.
DESCRIPTION
eta tac tries to apply tac to all the goals in the current goal list; replacing the goal list with the list of all the resulting subgoals. If it fails on a goal, it has no effect on that goal. It is an abbreviation for expand_list (TRYALL tac).
USES
For interactively constructing suitable compound tactics: in an interactive proof, the effect of e (tac1 THEN TRY tac2) can be obtained by e tac1 and then eta tac2.
SEEALSO
HOL  Trindemossen-1