Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-02 15:34:20 -0700 (Mon, 02 Jul 2001)
Revision: 3307
Log message:
- added rules applyEquality to intro resource
- many rules (e.g. letT and elimination rules for the intersection and union types)
produces equality hypotheses in the subgoals that rarely used in practice.
Now such rules thin these hypotheses by default.
To avoid this one can use doNotThinT = thinningT false.