src/ZF/Constructible/Formula.thy
2002-07-19 paulson 2002-07-19 Towards relativization and absoluteness of formula_rec
2002-07-17 paulson 2002-07-17 Expressing Lset and L without using length and arity; simplifies Separation proofs
2002-07-10 paulson 2002-07-10 Fixed quantified variable name preservation for ball and bex (bounded quants) Requires tweaking of other scripts. Also routine tidying.
2002-07-09 paulson 2002-07-09 better document preparation
2002-07-08 paulson 2002-07-08 more and simpler separation proofs
2002-07-05 paulson 2002-07-05 more internalized formulas and separation proofs
2002-07-04 paulson 2002-07-04 Constructible: some separation axioms
2002-07-04 paulson 2002-07-04 towards proving separation for L
2002-07-02 paulson 2002-07-02 Tidying and introduction of various new theorems
2002-06-24 paulson 2002-06-24 development and tweaks
2002-06-19 paulson 2002-06-19 new theory of inner models