--- 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"
--- 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:
--- 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";
--- 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);