Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 22:57:26 -0700 (Mon, 08 Apr 2002)
Revision: 3567
Log message:

      1. Redefined inverse image. Previously it was defined by introduction
         and elimination rules; now it can be rewritten with "setbvd_prop".
         Actually, after "setbvd_prop" is defined, the "inv_image" is somewhat
         unnecessary. I keep it here just in case that people may want to use
         the concept of inverse image sometimes.
      2. Fixed the error in the previous member elimination rule.
      

Changes	Path
+8 -5	metaprl/theories/czf/czf_itt_inv_image.ml
+4 -1	metaprl/theories/czf/czf_itt_inv_image.mli
+572 -351	metaprl/theories/czf/czf_itt_inv_image.prla