--- a/src/HOL/Prod.ML Tue Mar 26 17:15:54 1996 +0100
+++ b/src/HOL/Prod.ML Wed Mar 27 18:45:17 1996 +0100
@@ -232,6 +232,19 @@
addSEs [SigmaE]) 1);
qed "Sigma_mono";
+qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
+ (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
+
+qed_goal "Sigma_empty2" Prod.thy "Sigma A (%x.{}) = {}"
+ (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
+
+Addsimps [Sigma_empty1,Sigma_empty2];
+
+goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
+by (fast_tac (eq_cs addSIs [SigmaI] addSEs [SigmaE, Pair_inject]) 1);
+qed "mem_Sigma_iff";
+Addsimps [mem_Sigma_iff];
+
(*** Domain of a relation ***)