src/ZF/ZF.thy
2017-04-12 wenzelm 2017-04-12 merged
2017-04-10 wenzelm 2017-04-10 tuned text;
2017-04-09 wenzelm 2017-04-09 clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
2017-04-04 wenzelm 2017-04-04 allow to load this into "isabelle jedit -l HOL";
2016-09-16 wenzelm 2016-09-16 more symbols;
2016-01-12 wenzelm 2016-01-12 clarified axiomatization versus definitions; eliminated old defs; more symbols;
2015-12-30 wenzelm 2015-12-30 clarified syntax;
2015-12-30 wenzelm 2015-12-30 clarified print modes;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-02-10 wenzelm 2014-02-10 prefer vacuous definitional type classes over axiomatic ones;
2012-08-08 wenzelm 2012-08-08 proper axiomatization of "mem" -- do not leave it formally unspecified;
2012-07-24 wenzelm 2012-07-24 clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
2012-03-16 wenzelm 2012-03-16 modernized axiomatization; eliminated odd 'finalconsts';
2012-03-13 paulson 2012-03-13 Structured proofs concerning the square of an infinite cardinal
2012-03-06 paulson 2012-03-06 mathematical symbols instead of ASCII
2012-03-01 paulson 2012-03-01 Removal of obsolete ML bindings
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-08-11 wenzelm 2011-08-11 redundant use of misc_legacy.ML;
2011-02-18 wenzelm 2011-02-18 modernized specifications;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-11-26 wenzelm 2010-11-26 prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
2010-09-03 wenzelm 2010-09-03 turned eta_contract into proper configuration option;
2010-08-27 wenzelm 2010-08-27 expanded some aliases from structure Unsynchronized;
2010-08-18 haftmann 2010-08-18 deglobalization
2010-07-12 wenzelm 2010-07-12 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
2010-06-11 haftmann 2010-06-11 avoid references to old constdefs
2010-02-11 wenzelm 2010-02-11 numeral syntax: clarify parse trees vs. actual terms; modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2010-02-10 wenzelm 2010-02-10 modernized translations;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2008-07-29 ballarin 2008-07-29 Lemmas added
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-10-03 wenzelm 2007-10-03 avoid unnamed infixes;
2007-05-31 wenzelm 2007-05-31 tuned ML setup;
2006-01-29 wenzelm 2006-01-29 declare atomize/defn for Ball;
2005-12-15 wenzelm 2005-12-15 removed obsolete/unused setup_induction;
2005-10-07 wenzelm 2005-10-07 replaced _K by dummy abstraction;
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
2004-06-08 paulson 2004-06-08 Groups, Rings and supporting lemmas
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2003-10-10 paulson 2003-10-10 finalconsts
2003-07-10 paulson 2003-07-10 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new variable
2003-06-27 paulson 2003-06-27 Conversion of AllocBase to new-style
2003-01-15 paulson 2003-01-15 more new-style theories
2002-05-23 paulson 2002-05-23 new definition of "apply" and new simprule "beta_if"
2002-05-13 paulson 2002-05-13 quotes around types
2002-05-08 paulson 2002-05-08 the new predicate "relation"
2002-05-07 wenzelm 2002-05-07 tuned;
2002-02-15 paulson 2002-02-15 a new definition of "restrict"
2002-01-15 paulson 2002-01-15 split can now be unfolded even with one argument
2001-12-19 paulson 2001-12-19 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-05-21 paulson 2001-05-21 fixed the X-symbol syntax for lambda
2001-03-30 paulson 2001-03-30 the one-point rule for bounded quantifiers