--- a/src/ZF/pair.ML Thu Aug 06 10:37:33 1998 +0200 +++ b/src/ZF/pair.ML Thu Aug 06 10:37:39 1998 +0200 @@ -106,6 +106,10 @@ Addsimps [Sigma_empty1, Sigma_empty2]; +Goal "A*B=0 <-> A=0 | B=0"; +by (Blast_tac 1); +qed "Sigma_empty_iff"; + (*** Projections: fst, snd ***)