src/ZF/pair.ML

 qed_goal "Sigma_empty2" ZF.thy "A*0 = 0"
  (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [Sigma_empty1, Sigma_empty2];
 
+Goal "A*B=0 <-> A=0 | B=0";
+by (Blast_tac 1);
+qed "Sigma_empty_iff";
+
 
 (*** Projections: fst, snd ***)
 
 qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a"
  (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);