src/ZF/pair.ML
1993-09-17 lcp 1993-09-17 Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
1993-09-16 clasohm 1993-09-16 Initial revision