Parent Directory | Revision Log
Links to HEAD: | (view) (download) (annotate) |
Sticky Revision: |
- 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?).
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.
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.
ViewVC Help | |
Powered by ViewVC 1.1.26 |