e : tactic -> proof
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
HOL  Kananaskis-14