diff -r 26f64e7a67b5 -r 74ab7c0980c7 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Nov 13 15:42:57 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Nov 13 15:42:58 2006 +0100
@@ -9,19 +9,21 @@
 imports Main
 begin
 
-section {* Definitional equality rewrites *}
+section {* Definitional rewrites *}
 
 instance set :: (eq) eq ..
 
 lemma [code target: Set]:
-  "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
+  "(A = B) \<longleftrightarrow> (A \<subseteq> B \<and> B \<subseteq> A)"
   by blast
 
 lemma [code func]:
-  "Code_Generator.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
+  "Code_Generator.eq A B \<longleftrightarrow> (A \<subseteq> B \<and> B \<subseteq> A)"
   unfolding eq_def by blast
 
-declare bex_triv_one_point1 [symmetric, standard, code]
+lemma [code]:
+  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
+  unfolding bex_triv_one_point1 ..
 
 
 section {* HOL definitions *}