src/ZF/ZF.thy
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
1995-05-10 nipkow 1995-05-10 Modified translation for pattern abstraction.
1995-05-04 lcp 1995-05-04 Added pattern-matching code from CHOL/Prod.thy. Changed definitions so that split is now defined in terms of fst, snd. Now split is polymorphic. Deleted fsplit, as split(...)::o gives a similar effect -- NOT identical though, as fsplit(P,z) implied that z was a pair, while split(P,z) means only P(fst(z),snd(z)).
1994-11-03 lcp 1994-11-03 ZF: NEW DEFINITION OF PI(A,B) Was Pi(A,B) == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f} Now function(r) == ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y') Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}" This simplifies many proofs, since (a) the top-level definition has fewer bound variables (b) the "total" and "function" properties are separated (c) the awkward EX! quantifier is eliminated. ZF/ZF.thy/function: new definition
1994-10-31 lcp 1994-10-31 ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
1994-10-12 wenzelm 1994-10-12 fixed infix names in print_translations;
1994-09-21 wenzelm 1994-09-21 minor cleanup, added 'syntax' section;
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc.
1994-05-03 lcp 1994-05-03 removal of obsolete type-declaration syntax
1993-10-25 wenzelm 1993-10-25 added white-space; made ~: a fake infix;
1993-10-11 wenzelm 1993-10-11 "The" now a binder, removed translation; improved encoding and translations of tuples; added parse rules for -> and *, removed ndependent_tr;
1993-10-07 lcp 1993-10-07 added ~: for "not in"
1993-09-16 clasohm 1993-09-16 Initial revision