src/ZF/Constructible/Formula.thy
2017-04-09 wenzelm 2017-04-09 clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.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;
2014-11-01 wenzelm 2014-11-01 eliminated spurious semicolons;
2012-03-15 paulson 2012-03-15 replacing ":" by "\<in>"
2012-03-06 paulson 2012-03-06 More mathematical symbols for ZF examples
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
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
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2002-11-19 paulson 2002-11-19 stylistic tweaks
2002-10-30 paulson 2002-10-30 simpler separation/replacement proofs
2002-10-17 paulson 2002-10-17 Cosmetic changes suggested by writing the paper. Deleted some redundant arity proofs
2002-10-14 paulson 2002-10-14 tidying and reorganization
2002-10-09 paulson 2002-10-09 Re-organization of Constructible theories
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-08-21 paulson 2002-08-21 new proof needed now
2002-08-16 paulson 2002-08-16 Relativized right up to L satisfies V=L!
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