Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-08-29 17:56:48 -0700 (Tue, 29 Aug 2000)
Revision: 3052
Log message:
Two changes.
1. expand () now does sloppy expansion, so that proofs
can be replayed even if the goal of a proof has changed.
This also means that proof copy/paste should work.
2. I fixed up CZF. This is a pretty cool set theory, where
we get the usual ZF axioms (except excluded middle). The
normal things like numbers can be coded in the usual
way, except we get decidability of number equality and
other constructive ideas. Reals can be coded with
Dedekind cuts according to Aczel. This theory is the
basic set theory with just the axioms. Before going on,
it is probably a good idea to stratify the sets with
levels, so we can formalize the notion of classes.