Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-23 23:54:36 -0800 (Sat, 23 Mar 2002)
Revision: 3545
Log message:

      Added the definition for "set builder", i.e., the image of a set s
      under some function f: { f(x) | x in s }. I consider this as a necessity
      for the set theory.
      
      The "set builder" is defined by a "set-induction" rewrite rule. Also
      added and proved properties for it.
      

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