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