1.1 --- a/src/ZF/AC/AC15_WO6.thy	Fri Jan 18 17:45:19 2002 +0100
     1.2 +++ b/src/ZF/AC/AC15_WO6.thy	Fri Jan 18 17:46:17 2002 +0100
     1.3 @@ -269,7 +269,7 @@
     1.4  apply (drule bspec, assumption)
     1.5  apply (elim conjE)
     1.6  apply (erule lemma_aux [THEN exE], assumption)
     1.7 -apply (simp add: the_element)
     1.8 +apply (simp add: the_equality)
     1.9  done
    1.10  
    1.11  theorem AC13_AC1: "AC13(1) ==> AC1"

     2.1 --- a/src/ZF/AC/AC_Equiv.thy	Fri Jan 18 17:45:19 2002 +0100
     2.2 +++ b/src/ZF/AC/AC_Equiv.thy	Fri Jan 18 17:46:17 2002 +0100
     2.3 @@ -151,12 +151,9 @@
     2.4  apply (erule id_bij [THEN bij_ordertype_vimage])
     2.5  done
     2.6  
     2.7 -lemma the_element: "(THE z. {x}={z}) = x"
     2.8 -by (fast elim!: singleton_eq_iff [THEN iffD1, symmetric])
     2.9 -
    2.10  lemma lam_sing_bij: "(\<lambda>x \<in> A. {x}) \<in> bij(A, {{x}. x \<in> A})"
    2.11  apply (rule_tac d = "%z. THE x. z={x}" in lam_bijective)
    2.12 -apply (auto simp add: the_element) 
    2.13 +apply (auto simp add: the_equality)
    2.14  done
    2.15  
    2.16  lemma inj_strengthen_type: 

     3.1 --- a/src/ZF/Epsilon.ML	Fri Jan 18 17:45:19 2002 +0100
     3.2 +++ b/src/ZF/Epsilon.ML	Fri Jan 18 17:46:17 2002 +0100
     3.3 @@ -311,13 +311,9 @@
     3.4  by (Simp_tac 1);
     3.5  qed "transrec2_0";
     3.6  
     3.7 -Goal "(THE j. i=j) = i";
     3.8 -by (Blast_tac 1);
     3.9 -qed "THE_eq";
    3.10 -
    3.11  Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
    3.12  by (rtac (transrec2_def RS def_transrec RS trans) 1);
    3.13 -by (simp_tac (simpset() addsimps [THE_eq, if_P]) 1);
    3.14 +by (simp_tac (simpset() addsimps [the_equality, if_P]) 1);
    3.15  by (Blast_tac 1);
    3.16  qed "transrec2_succ";
    3.17  

     4.1 --- a/src/ZF/pair.ML	Fri Jan 18 17:45:19 2002 +0100
     4.2 +++ b/src/ZF/pair.ML	Fri Jan 18 17:46:17 2002 +0100
     4.3 @@ -12,6 +12,7 @@
     4.4  by (resolve_tac [extension RS iff_trans] 1);
     4.5  by (Blast_tac 1) ;
     4.6  qed "singleton_eq_iff";
     4.7 +AddIffs [singleton_eq_iff];
     4.8  
     4.9  Goal "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)";
    4.10  by (resolve_tac [extension RS iff_trans] 1);