lcp [Thu, 03 Nov 1994 16:39:41 +0100] rev 695
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
lcp [Thu, 03 Nov 1994 16:05:22 +0100] rev 694
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
lcp [Thu, 03 Nov 1994 13:42:39 +0100] rev 693
ZF/Perm/inj_converse_fun: tidied; removed uses of PiI/E
ZF/Perm/comp_fun: tidied; removed use of PiI
lcp [Thu, 03 Nov 1994 12:43:42 +0100] rev 692
ZF/InfDatatype/fun_Vcsucc: removed use of PiE
lcp [Thu, 03 Nov 1994 12:39:39 +0100] rev 691
ZF/func: tidied many proofs, using new definition of Pi(A,B)
ZF/func/PiI,PiE: removed
ZF/func/Pi_iff_old: new
ZF/func/Pi_memberD: new; simpler, replaces memberPiE
lcp [Thu, 03 Nov 1994 12:35:41 +0100] rev 690
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
lcp [Thu, 03 Nov 1994 12:30:55 +0100] rev 689
ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp [Thu, 03 Nov 1994 12:26:59 +0100] rev 688
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
lcp [Thu, 03 Nov 1994 12:23:19 +0100] rev 687
ZF/domrange/converse_iff: new
lcp [Thu, 03 Nov 1994 12:06:37 +0100] rev 686
ZF/upair/theI2: new
lcp [Thu, 03 Nov 1994 11:58:16 +0100] rev 685
ZF/equalities/domain_converse,range_converse,
prod_Un_distrib2,prod_Int_distrib2: new
lcp [Thu, 03 Nov 1994 11:52:04 +0100] rev 684
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp [Thu, 03 Nov 1994 11:45:41 +0100] rev 683
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
clasohm [Thu, 03 Nov 1994 08:34:53 +0100] rev 682
added warning message
"Currently parsed expression could be extremely ambiguous."