src/ZF/Constructible/L_axioms.thy
2002-07-08 paulson 2002-07-08 more and simpler separation proofs
2002-07-08 paulson 2002-07-08 Defining a meta-existential quantifier. Using it to streamline reflection proofs.
2002-07-08 paulson 2002-07-08 reflection for more internal formulas
2002-07-05 paulson 2002-07-05 more internalized formulas and separation proofs
2002-07-05 paulson 2002-07-05 more separation instances
2002-07-04 paulson 2002-07-04 More use of relativized quantifiers
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-07-01 paulson 2002-07-01 more use of relativized quantifiers list_closed
2002-06-19 paulson 2002-06-19 new theory of inner models