src/ZF/ZF.thy
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
2000-09-15 wenzelm 2000-09-15 tuned spacing of symbols syntax; enabled langle and rangle in xsymbols syntax;
2000-08-24 paulson 2000-08-24 added some xsymbols, and tidied
1999-03-10 wenzelm 1999-03-10 HTML output;
1999-01-07 paulson 1999-01-07 if-then-else syntax for ZF
1997-10-20 wenzelm 1997-10-20 local;
1997-10-16 wenzelm 1997-10-16 global;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-22 wenzelm 1997-09-22 tuned pattern syntax;
1997-04-29 wenzelm 1997-04-29 deactivated new symbols (not yet printable on xterm, emacs);
1997-04-29 wenzelm 1997-04-29 added \<langle>, \<rangle> symbols syntax;
1997-04-02 paulson 1997-04-02 Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
1997-01-23 wenzelm 1997-01-23 added symbols syntax;
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-12-02 wenzelm 1996-12-02 removed out-dated comment;
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-12-09 clasohm 1995-12-09 removed quotes from consts and syntax sections
1995-06-22 clasohm 1995-06-22 removed \...\ inside strings