next up previous contents index
Next: Rule Constructors Up: Appendix A: Summary Previous: General Notes

Refinement Functions


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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995