Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-03 18:19:09 -0800 (Sun, 03 Mar 2002)
Revision: 3526
Log message:

      1. Defined functionality in the sense of equivalence relations,
         which is distinct from the functionality for equality.
      2. Added and proved properties of equivalence functionality.
      3. Added and proved functionality properties of equivalence relations
         (both equivalence functionality and equality functionality).
      4. Updated the substitution rules and tactics.
      
      Tactics for equivalence relations:
        equivFunSetT, equivFunMemT, equivRefT, equivSymT,
        equivTransT, equivSubstT
      
      TODO:
        1. Might need to define terms for functionality judgments on
           dependent types (i.e., equiv_dfun_prop).
        2. Implement equivalence class later.
      

Changes	Path
+233 -18	metaprl/theories/czf/czf_itt_equiv.ml
+28 -0	metaprl/theories/czf/czf_itt_equiv.mli
+7940 -1958	metaprl/theories/czf/czf_itt_equiv.prla