refine : refinement -> goalstack

SYNOPSIS
Applies a refinement to the current goalstack.

DESCRIPTION
The call refine r applies the refinement r to the current goalstate, adding the resulting goalstate at the head of the current goalstack list. (A goalstate consists of a list of subgoals as well as justification and metavariable information.)

FAILURE CONDITIONS
Fails if the refinement fails.

COMMENTS
Most users will not want to handle refinements explicitly. Usually one just applies a tactic to the first goal in a goalstate.