1\DOC e
2
3\TYPE {e : tactic -> proof}
4
5\SYNOPSIS
6Applies a tactic to the current goal, stacking the resulting subgoals.
7
8\DESCRIBE
9The function {e} is part of the subgoal package. It is an abbreviation for
10{expand}. For a description of the subgoal package, see {set_goal}.
11
12\FAILURE
13As for {expand}.
14
15\USES
16Doing a step in an interactive goal-directed proof.
17
18\SEEALSO
19proofManagerLib.set_goal, proofManagerLib.restart,
20proofManagerLib.backup,proofManagerLib.restore, proofManagerLib.save,
21proofManagerLib.set_backup,proofManagerLib.expand, proofManagerLib.expandf,
22proofManagerLib.p,proofManagerLib.top_thm, proofManagerLib.top_goal.
23
24\ENDDOC
25