next up previous contents index
Next: Substitution Up: Rewriting Previous: Declaring Relations



There are two types of justifications.

Computational Justifications
  These indicate precise applications of the forward and reverse direct computation rules  . They are comparatively very fast and generate no well formedness subgoals. The rewrite package uses these whenever possible.
Tactic Justifications
  These are more generally applicable. Extensive use is made of lemmas, and many well formedness subgoals are generated.

Conversions generating both types of justification can be freely intermixed; the system takes care of converting computational justifications to tactic justifications when necessary.

Karla Consroe
Wed Oct 23 13:48:45 EDT 1996