1.1 --- a/src/ZF/pair.thy	Tue Jun 01 18:52:38 2004 +0200
     1.2 +++ b/src/ZF/pair.thy	Wed Jun 02 17:35:08 2004 +0200
     1.3 @@ -149,6 +149,18 @@
     1.4  lemma splitD: "split(R,<a,b>) ==> R(a,b)"
     1.5  by (simp add: split_def)
     1.6  
     1.7 +text {*
     1.8 +  \bigskip Complex rules for Sigma.
     1.9 +*}
    1.10 +
    1.11 +lemma split_paired_Bex_Sigma [simp]:
    1.12 +     "(\<exists>z \<in> Sigma(A,B). P(z)) <-> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
    1.13 +by blast
    1.14 +
    1.15 +lemma split_paired_Ball_Sigma [simp]:
    1.16 +     "(\<forall>z \<in> Sigma(A,B). P(z)) <-> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
    1.17 +by blast
    1.18 +
    1.19  ML
    1.20  {*
    1.21  val singleton_eq_iff = thm "singleton_eq_iff";