src/ZF/ZF.thy
 1996-02-06 clasohm 1996-02-06 expanded tabs file | diff | annotate 1995-12-09 clasohm 1995-12-09 removed quotes from consts and syntax sections file | diff | annotate 1995-06-22 clasohm 1995-06-22 removed \...\ inside strings file | diff | annotate 1995-05-10 nipkow 1995-05-10 Modified translation for pattern abstraction. file | diff | annotate 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)). file | diff | annotate 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. : f} Now function(r) == ALL x y. :r --> (ALL 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 file | diff | annotate 1994-10-31 lcp 1994-10-31 ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B} file | diff | annotate 1994-10-12 wenzelm 1994-10-12 fixed infix names in print_translations; file | diff | annotate 1994-09-21 wenzelm 1994-09-21 minor cleanup, added 'syntax' section; file | diff | annotate 1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections file | diff | annotate 1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc. file | diff | annotate 1994-05-03 lcp 1994-05-03 removal of obsolete type-declaration syntax file | diff | annotate 1993-10-25 wenzelm 1993-10-25 added white-space; made ~: a fake infix; file | diff | annotate 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; file | diff | annotate 1993-10-07 lcp 1993-10-07 added ~: for "not in" file | diff | annotate 1993-09-16 clasohm 1993-09-16 Initial revision file | diff | annotate