src/ZF/ZF.thy
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