ViewVC logotype

Revision 3568

Jump to revision: Previous Next
Author: xiny
Date: Tue Apr 9 05:57:54 2002 UTC (19 years, 3 months ago)
Changed paths: 3
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.

Changed paths

Path Details
Directorymetaprl/theories/czf/czf_itt_set_bvd.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_set_bvd.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_set_bvd.prla modified , text changed

  ViewVC Help
Powered by ViewVC 1.1.26