# HG changeset patch
# User paulson
# Date 1011372377 -3600
# Node ID 2f5edb146f7eebc826055745a4366ff118e4b615
# Parent  f8f0807e5a5e1d60159820e5efcfa972409c2aec
tidied

diff -r f8f0807e5a5e -r 2f5edb146f7e src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Fri Jan 18 17:45:19 2002 +0100
+++ b/src/ZF/AC/AC15_WO6.thy	Fri Jan 18 17:46:17 2002 +0100
@@ -269,7 +269,7 @@
 apply (drule bspec, assumption)
 apply (elim conjE)
 apply (erule lemma_aux [THEN exE], assumption)
-apply (simp add: the_element)
+apply (simp add: the_equality)
 done
 
 theorem AC13_AC1: "AC13(1) ==> AC1"
diff -r f8f0807e5a5e -r 2f5edb146f7e src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Fri Jan 18 17:45:19 2002 +0100
+++ b/src/ZF/AC/AC_Equiv.thy	Fri Jan 18 17:46:17 2002 +0100
@@ -151,12 +151,9 @@
 apply (erule id_bij [THEN bij_ordertype_vimage])
 done
 
-lemma the_element: "(THE z. {x}={z}) = x"
-by (fast elim!: singleton_eq_iff [THEN iffD1, symmetric])
-
 lemma lam_sing_bij: "(\<lambda>x \<in> A. {x}) \<in> bij(A, {{x}. x \<in> A})"
 apply (rule_tac d = "%z. THE x. z={x}" in lam_bijective)
-apply (auto simp add: the_element) 
+apply (auto simp add: the_equality)
 done
 
 lemma inj_strengthen_type: 
diff -r f8f0807e5a5e -r 2f5edb146f7e src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Fri Jan 18 17:45:19 2002 +0100
+++ b/src/ZF/Epsilon.ML	Fri Jan 18 17:46:17 2002 +0100
@@ -311,13 +311,9 @@
 by (Simp_tac 1);
 qed "transrec2_0";
 
-Goal "(THE j. i=j) = i";
-by (Blast_tac 1);
-qed "THE_eq";
-
 Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
 by (rtac (transrec2_def RS def_transrec RS trans) 1);
-by (simp_tac (simpset() addsimps [THE_eq, if_P]) 1);
+by (simp_tac (simpset() addsimps [the_equality, if_P]) 1);
 by (Blast_tac 1);
 qed "transrec2_succ";
 
diff -r f8f0807e5a5e -r 2f5edb146f7e src/ZF/pair.ML
--- a/src/ZF/pair.ML	Fri Jan 18 17:45:19 2002 +0100
+++ b/src/ZF/pair.ML	Fri Jan 18 17:46:17 2002 +0100
@@ -12,6 +12,7 @@
 by (resolve_tac [extension RS iff_trans] 1);
 by (Blast_tac 1) ;
 qed "singleton_eq_iff";
+AddIffs [singleton_eq_iff];
 
 Goal "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)";
 by (resolve_tac [extension RS iff_trans] 1);