SPLIT_LT : int -> list_tactic * list_tactic -> list_tactic
STRUCTURE
SYNOPSIS
Splits a list of goals into two and applies a list-tactic to each part
DESCRIPTION
For list-tactics ltac1 and ltac2, integer n and goal list gl, the application SPLIT_LT n (ltac1, ltac2) gl applies ltac1 to the first n goals in gl, and ltac2 to the remainder. If n is negative, ltac1 is applied to the goals before the last -n, and ltac2 to the last -n goals.
FAILURE
The application SPLIT_LT n (ltac1, ltac2) never fails, but when applied to a goal list, it fails if the index n is (in absolute value) larger then the length of the list, or if either of the list-tactics ltac1 and ltac2 fails.
EXAMPLE
To apply tactic tac1 to a goal, and then to apply tac2 to all resulting subgoals except the first, use
  tac1 THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS tac2)
SEEALSO
HOL  Kananaskis-13