# HG changeset patch
# User haftmann
# Date 1172216363 -3600
# Node ID b410755a0d5a4b4d3a6b6ff8867f99a82df03be8
# Parent  a4e82dd93202a760989a6b67f11332956181a577
slightly tuned

diff -r a4e82dd93202 -r b410755a0d5a src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Fri Feb 23 08:39:22 2007 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Fri Feb 23 08:39:23 2007 +0100
@@ -50,15 +50,15 @@
 
 definition
   member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
-  "member xs x = (x \<in> set xs)"
+  "member xs x \<longleftrightarrow> x \<in> set xs"
 
 definition
   insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "insertl x xs = (if member xs x then xs else x#xs)"
 
 lemma
-  [code target: List]: "member [] y = False"
-  and [code target: List]: "member (x#xs) y = (y = x \<or> member xs y)"
+  [code target: List]: "member [] y \<longleftrightarrow> False"
+  and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
 unfolding member_def by (induct xs) simp_all
 
 fun
@@ -172,7 +172,7 @@
 section {* Isomorphism proofs *}
 
 lemma iso_member:
-  "member xs x = (x \<in> set xs)"
+  "member xs x \<longleftrightarrow> x \<in> set xs"
   unfolding member_def mem_iff ..
 
 lemma iso_insert:
@@ -316,9 +316,6 @@
   Bex \<equiv> Blex
   filter_set \<equiv> filter
 
-code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-  image Union Inter UNION INTER Ball Bex filter_set (SML -)
-
 
 subsection {* type serializations *}