`refine: rule tactic.`-
This function refines a proof according to a given rule.
`refine_using_prl_rule: tok tactic.`-
This function parses the token as a rule in the context of the
given proof. The proof is then refined via this rule.

Thu Sep 14 08:45:18 EDT 1995