e
proofManagerLib.e : tactic -> proof
Applies a tactic to the current goal, stacking the resulting subgoals.
The function e is part of the subgoal package. It is an abbreviation
for expand. For a description of the subgoal package, see set_goal.
Failure
As for expand.
Doing a step in an interactive goal-directed proof.
See also
proofManagerLib.set_goal,
proofManagerLib.restart,
proofManagerLib.backup,
proofManagerLib.redo,
proofManagerLib.restore,
proofManagerLib.save,
proofManagerLib.set_backup,
proofManagerLib.expand,
proofManagerLib.expandf,
proofManagerLib.p,
proofManagerLib.top_thm,
proofManagerLib.top_goal