src/ZF/Constructible/L_axioms.thy
2002-08-16 paulson 2002-08-16 Various tweaks of the presentation
2002-08-16 paulson 2002-08-16 Relativized right up to L satisfies V=L!
2002-08-13 paulson 2002-08-13 In ZF/Constructible, moved many results from Satisfies_absolute, etc., to the new theory Internalize.thy
2002-08-12 paulson 2002-08-12 Lots of new results concerning recursive datatypes, towards absoluteness of "satisfies"
2002-07-31 paulson 2002-07-31 some progress towards "satisfies"
2002-07-30 paulson 2002-07-30 better sats rules for higher-order operators
2002-07-29 wenzelm 2002-07-29 tuned;
2002-07-29 wenzelm 2002-07-29 eliminate open locales and special ML code;
2002-07-24 paulson 2002-07-24 tweaks, aiming towards relativization of "satisfies"
2002-07-17 paulson 2002-07-17 Expressing Lset and L without using length and arity; simplifies Separation proofs
2002-07-16 paulson 2002-07-16 instantiation of locales M_trancl and M_wfrank; proofs of list_replacement{1,2}
2002-07-12 paulson 2002-07-12 new definitions of fun_apply and M_is_recfun
2002-07-11 paulson 2002-07-11 Separation/Replacement up to M_wfrank!
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 More relativization, reflection and proofs of separation
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