Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-24 00:21:13 -0800 (Sun, 24 Mar 2002)
Revision: 3546
Log message:

      Added the module for the inverse image of set t in set s under function f:
         { x in s | f(x) in t }
      
      I didn't find a direct way to define it, so I define it using axioms.
      

Changes	Path
Added	metaprl/theories/czf/czf_itt_inv_image.ml
Properties	metaprl/theories/czf/czf_itt_inv_image.ml
Added	metaprl/theories/czf/czf_itt_inv_image.mli
Properties	metaprl/theories/czf/czf_itt_inv_image.mli
Added	metaprl/theories/czf/czf_itt_inv_image.prla
Properties	metaprl/theories/czf/czf_itt_inv_image.prla