op THEN_LT : tactic * list_tactic -> tactic op THEN_LT : list_tactic * list_tactic -> list_tactic
If ltac1 and ltac2 are list-tactics, then ltac1 THEN_LT ltac2 is a list-tactic which applies ltac1 to a goal list, and if it does not fail, applies ltac2 to the resulting list of goals.
The tactic tac THEN_LT ltac fails if tac fails when applied to the goal, or if ltac fails when applied to the resulting subgoal list.
The list-tactic ltac1 THEN_LT ltac2 fails if ltac1 fails when applied to the goal list, or if ltac2 fails when applied to the goal list result of ltac1.
Where tac1 is a tactic and tacs2 is a list of tactics, tac1 THEN_LT NULL_OK_LT (TACS_TO_LT tacs2) is equivalent to tac1 THENL tacs2
Where tac is a tactic, tac THEN_LT REVERSE_LT is equivalent to REVERSE tac