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