Previous: Declaring Relations
There are two types of justifications.
Conversions generating both types of justification can be freely
intermixed; the system takes care of converting computational
justifications to tactic justifications when necessary.
- Computational Justifications
These indicate precise applications of the forward and reverse direct
. 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.
Wed Oct 23 13:48:45 EDT 1996