was to execute command *A*, then execute command *B*. ie
*B* was executed on whatever was the current subgoal after
*A* finished. If *A* left several subgoals, then *B*
was only executed on the first. If *A* discharged its goal, then
*B* was executed on whatever proof obligation surfaced next.

For this alpha release, the `Then` tactical has been modified
to reflect more accurately the LCF spirit.

Morally, the effect of *A* `Then` *B*
should be to execute *A*, then execute *B* for each of the subgoals
generated by *A*, if there are any.

*
Unfortunately, if A leaves us with more than one subgoal,
running B on the first may leave the others
inaccessible. However, the new implementation tags these inaccessible
subgoals with an instruction to execute B automatically as soon
as each one resurfaces. Hence B is executed on each subgoal
generated by A.
*

*
It may be the case that B does not complete the proof of
A's first subgoal, and that you may need to intervene. Once you
have finished off the branch and the next A-subgoal comes up,
B will happen to it before your eyes. This may prove slightly
disconcerting.
*

*
Here's an example:
*

Lego> Goal plus: nat->nat->nat; Goal plus ?0 : nat->nat->nat Lego> Induction 1 Then intros; Refine by nat_elim ([_:nat]nat->nat) ?1 : nat->nat ?2 : nat->(nat->nat)->nat->nat executing delayed Then tactic... (* intros for ?1 *) intros (1) H : nat ?3 : nat Lego> Refine H; (* user finishes off ?1 proof *) Refine by H Discharge.. H ?2 : nat->(nat->nat)->nat->nat executing delayed Then tactic... (* intros for ?2 *) intros (3) x1 : nat x1_ih : nat->nat H : nat ?4 : nat Lego> Refine (suc (x1_ih H)); Refine by suc (x1_ih H) Discharge.. H x1_ih x1 *** QED ***

*
Then behaves correctly with respect to Undo.
Undo n undoes n user commands. A tactical
compound counts as a single command. If you undo a command which was
followed by the automatic execution of a delayed Then tactic,
you will still return to the state before your command, incidentally
undoing the delayed tactic and replacing the tag on its goal.
*

*
One slight quirk is what happens to
A Then B if A succeeds but B fails.
Morally, if any instance of B fails, the whole A Then
B should fail. However, the latency in executing some
B's makes this impractical. Hence our A Then
B really behaves like A Then
(Try B).
*

*
An ideal implementation of Then requires the ability to
switch between different branches of the proof in their different
contexts. This is difficult because implicit synthesis of existential
variables can cause interference between branches. What has been done
falls well short of this ideal, but it nonetheless a powerful and
effort-saving tool.
*