--- 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 ***)