ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_set_bvd.ml

Parent Directory Parent Directory | Revision Log Revision Log

Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 3591 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
File length: 4155 byte(s)
Diff to previous 3568
- Added an option to be have "THEORIES=all" in mk/config
(instead of THEORIES="long list of theories").
I will change all my nightly scripts to use THEORIES=all.

- Added mc to the default list of TEXTHEORIES. Added a file all-bodies.tex
that would automatically contain \inputs corresponding to TEXTHEORIES.
(Before this change we had to update all-theories.tex by hands whenever TEXTHEORIES
was changed).

- Minor fixes in some display forms.

- Removed theories/caml that never had anything useful.

- Removed a few files from theories/ocaml_doc that seemed to be there by accident
(Jason, can you confirm?).

Revision 3568 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 9 05:57:54 2002 UTC (19 years, 2 months ago) by xiny
File length: 4161 byte(s)
Diff to previous 3545
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.

Revision 3545 - (view) (download) (annotate) - [select for diffs]
Added Sun Mar 24 07:54:36 2002 UTC (19 years, 3 months ago) by xiny
File length: 2608 byte(s)
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.

This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26