ALLGOALS : tactic -> list_tactic

- STRUCTURE
- SYNOPSIS
- Applies a tactic to every goal in a list
- DESCRIPTION
- If tac is a tactic, ALLGOALS tac is a list-tactic which applies the tactic tac to all the goals in the given list.
- FAILURE
- The application of ALLGOALS to a tactic never fails. The resulting list-tactic fails if tac fails when applied to any of the goals in the given list.
- EXAMPLE
- Where tac1 and tac2 are tactics, tac1 THEN_LT ALLGOALS tac2 is equivalent to tac1 THEN tac2
- SEEALSO

HOL Kananaskis-13