----------------------------------------------------------------------
SPLIT_LT                                                    (Tactical)
----------------------------------------------------------------------
SPLIT_LT : int -> list_tactic * list_tactic -> list_tactic

SYNOPSIS
Splits a list of goals into two and applies a list-tactic to each part

KEYWORDS
list-tactic.

DESCRIBE
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
Tactical.THEN_LT, Tactical.ALL_LT, Tactical.ALLGOALS.

----------------------------------------------------------------------