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