- STRUCTURE
- SYNOPSIS
Applies a tactic to the current goal, stacking the resulting subgoals.
- DESCRIPTION
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.
- USES
Doing a step in an interactive goal-directed proof.
- SEEALSO
set_goal,
restart,
backup,
restore,
save,
set_backup,
expand,
expandf,
p,
top_thm,
top_goal