src/ZF/Constructible/Relative.thy
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2015-03-23 wenzelm 2015-03-23 prefer local fixes;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-11-01 wenzelm 2014-11-01 eliminated spurious semicolons;
2013-06-26 wenzelm 2013-06-26 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context; even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac; adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);
2012-03-15 paulson 2012-03-15 replacing ":" by "\<in>"
2012-03-06 paulson 2012-03-06 More mathematical symbols for ZF examples
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2007-04-15 wenzelm 2007-04-15 read prop as prop, not term;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 tuned specifications;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-11-08 paulson 2002-11-08 Polishing. lambda_abs2 doesn't need an instance of replacement various renamings & restructurings
2002-10-30 paulson 2002-10-30 simpler separation/replacement proofs
2002-10-09 paulson 2002-10-09 Re-organization of Constructible theories
2002-10-04 paulson 2002-10-04 Various simplifications of the Constructible theories
2002-10-01 paulson 2002-10-01 Numerous cosmetic changes, prompted by the new simplifier
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-09-10 paulson 2002-09-10 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
2002-09-10 paulson 2002-09-10 tweaks
2002-08-28 paulson 2002-08-28 completion of the consistency proof for AC
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-08-22 paulson 2002-08-22 tweaked
2002-08-16 paulson 2002-08-16 Relativized right up to L satisfies V=L!
2002-07-31 paulson 2002-07-31 tweaks involving Separation
2002-07-30 paulson 2002-07-30 better sats rules for higher-order operators
2002-07-29 wenzelm 2002-07-29 eliminate open locales and special ML code;
2002-07-25 paulson 2002-07-25 More lemmas, working towards relativization of "satisfies"
2002-07-24 paulson 2002-07-24 tweaks, aiming towards relativization of "satisfies"
2002-07-19 paulson 2002-07-19 Absoluteness of the function "nth"
2002-07-16 wenzelm 2002-07-16 adapted locales;
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 towards relativization of "iterates" and "wfrec"
2002-07-12 paulson 2002-07-12 new definitions of fun_apply and M_is_recfun
2002-07-11 paulson 2002-07-11 tidied
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-09 paulson 2002-07-09 More Separation proofs
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 More use of relativized quantifiers
2002-07-04 paulson 2002-07-04 Constructible: some separation axioms
2002-07-04 paulson 2002-07-04 separation of M_axioms into M_triv_axioms and M_axioms
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-28 paulson 2002-06-28 class quantifiers (some) absoluteness and closure for WFrec-defined functions
2002-06-26 paulson 2002-06-26 new treatment of wfrec, replacing wf[A](r) by wf(r)
2002-06-26 paulson 2002-06-26 towards absoluteness of wfrec-defined functions
2002-06-24 paulson 2002-06-24 development and tweaks
2002-06-19 paulson 2002-06-19 new theory of inner models