src/ZF/Constructible/Separation.thy
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
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;
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-04-18 ballarin 2005-04-18 Cleaned up, now use interpretation.
2003-02-06 paulson 2003-02-06 changed ** to ## to avoid conflict with new comment syntax
2002-11-01 paulson 2002-11-01 tidy
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-09-11 paulson 2002-09-11 Streamlined proofs of instances of Separation
2002-09-10 paulson 2002-09-10 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
2002-08-16 paulson 2002-08-16 Relativized right up to L satisfies V=L!
2002-07-31 paulson 2002-07-31 some progress towards "satisfies"
2002-07-31 paulson 2002-07-31 separate "axioms" proofs: more flexible for locale reasoning
2002-07-29 wenzelm 2002-07-29 tuned;
2002-07-29 wenzelm 2002-07-29 eliminate open locales and special ML code;
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 tidied
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 and simpler separation proofs
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-08 paulson 2002-07-08 Defining a meta-existential quantifier. Using it to streamline reflection proofs.
2002-07-05 paulson 2002-07-05 more internalized formulas and separation proofs