ViewVC logotype

Revision 3545

Jump to revision: Previous Next
Author: xiny
Date: Sun Mar 24 07:54:36 2002 UTC (19 years, 4 months ago)
Changed paths: 3
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.

Changed paths

Path Details
Directorymetaprl/theories/czf/czf_itt_set_bvd.ml added
Directorymetaprl/theories/czf/czf_itt_set_bvd.mli added
Directorymetaprl/theories/czf/czf_itt_set_bvd.prla added

  ViewVC Help
Powered by ViewVC 1.1.26