SPLIT_LT
Tactical.SPLIT_LT : int -> list_tactic * list_tactic -> list_tactic
Splits a list of goals into two and applies a list-tactic to each part
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)