Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 00:46:33 -0800 (Tue, 02 Apr 2002)
Revision: 3559
Log message:
Changed def of homomorphisms and reproved all rules;
Added tactics "homIdT" and "homInvT".
Not finished yet. Will do the rest after fixing errors in subgroups
and cylic subgroups.
Changes | Path |
+55 -51 | metaprl/theories/czf/czf_itt_hom.ml |
+5 -3 | metaprl/theories/czf/czf_itt_hom.mli |
+6230 -3869 | metaprl/theories/czf/czf_itt_hom.prla |