eta

proofManagerLib.eta : tactic -> proof

Applies a tactic to all goals, on which it succeeds, in the current goal list, replacing the list with the resulting subgoals.

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).

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.

See also

proofManagerLib.expand_list, proofManagerLib.elt, Tactical.TRYALL, Tactical.TRY, proofManagerLib.eall, proofManagerLib.set_goal