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

      Added the definition for setbvd_prop. "set_bvd" and "setbvd_prop" are
      both methods for building sets. The former builds set { a(x) | x in s }
      from set s where a(x) is a function; the latter builds set
      { x in s | p(x) } from all elements x in s satisfying p(x). Both of
      them are very useful. The former is defined by set induction on s; the
      latter is defined by member introduction and elimination rules.
      

Changes	Path
+30 -3	metaprl/theories/czf/czf_itt_set_bvd.ml
+2 -2	metaprl/theories/czf/czf_itt_set_bvd.mli
+643 -406	metaprl/theories/czf/czf_itt_set_bvd.prla