clasohm [Wed, 09 Nov 1994 13:50:59 +0100] rev 697
changed warning for extremely ambiguous expressions
lcp [Thu, 03 Nov 1994 16:52:19 +0100] rev 696
Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
result.
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