elt : list_tactic -> proof
STRUCTURE
proofManagerLib
SYNOPSIS
Applies a list-tactic to the current goal list, replacing it with the resulting subgoals.
DESCRIPTION
The function
elt
is part of the subgoal package. It is an abbreviation for
expand_list
. For a description of the subgoal package, see
set_goal
.
FAILURE
As for
expand_list
.
USES
Doing a step in an interactive goal-directed proof, where the step may affect the list of goals produced by the previous step.
SEEALSO
expand_list
,
set_goal
HOL
Kananaskis-14