refine : refinement -> goalstack
Applies a refinement to the current goalstack.
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
- FAILURE CONDITIONS
Fails if the refinement fails.
Most users will not want to handle refinements explicitly. Usually one just
applies a tactic to the first goal in a goalstate.