1.1 --- a/src/ZF/OrderType.thy	Tue Jun 01 18:52:38 2004 +0200
     1.2 +++ b/src/ZF/OrderType.thy	Wed Jun 02 17:35:08 2004 +0200
     1.3 @@ -812,10 +812,11 @@
     1.4   prefer 2
     1.5   apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
     1.6  apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
     1.7 -apply (rule bexI)
     1.8 -prefer 2 apply (blast elim!: ltE)
     1.9 +apply (rule bexI [of _ i']) 
    1.10 +apply (rule bexI [of _ j']) 
    1.11  apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
    1.12  apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)
    1.13 +apply (simp_all add: lt_def) 
    1.14  done
    1.15  
    1.16  lemma omult_unfold:

     2.1 --- a/src/ZF/Ordinal.thy	Tue Jun 01 18:52:38 2004 +0200
     2.2 +++ b/src/ZF/Ordinal.thy	Wed Jun 02 17:35:08 2004 +0200
     2.3 @@ -293,7 +293,7 @@
     2.4  by (unfold Memrel_def, blast)
     2.5  
     2.6  lemma relation_Memrel: "relation(Memrel(A))"
     2.7 -by (simp add: relation_def Memrel_def, blast)
     2.8 +by (simp add: relation_def Memrel_def)
     2.9  
    2.10  (*The membership relation (as a set) is well-founded.
    2.11    Proof idea: show A<=B by applying the foundation axiom to A-B *)

     3.1 --- a/src/ZF/pair.thy	Tue Jun 01 18:52:38 2004 +0200
     3.2 +++ b/src/ZF/pair.thy	Wed Jun 02 17:35:08 2004 +0200
     3.3 @@ -149,6 +149,18 @@
     3.4  lemma splitD: "split(R,<a,b>) ==> R(a,b)"
     3.5  by (simp add: split_def)
     3.6  
     3.7 +text {*
     3.8 +  \bigskip Complex rules for Sigma.
     3.9 +*}
    3.10 +
    3.11 +lemma split_paired_Bex_Sigma [simp]:
    3.12 +     "(\<exists>z \<in> Sigma(A,B). P(z)) <-> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
    3.13 +by blast
    3.14 +
    3.15 +lemma split_paired_Ball_Sigma [simp]:
    3.16 +     "(\<forall>z \<in> Sigma(A,B). P(z)) <-> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
    3.17 +by blast
    3.18 +
    3.19  ML
    3.20  {*
    3.21  val singleton_eq_iff = thm "singleton_eq_iff";