code for {x:A. P(x)} and for fold

--- a/src/HOL/Library/Executable_Set.thy	Thu Dec 11 08:52:50 2008 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Thu Dec 11 08:53:53 2008 +0100
@@ -28,6 +28,10 @@
 lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   unfolding eq_set_def by auto
 
+(* FIXME allow for Stefan's code generator:
+declare set_eq_subset[code unfold]
+*)
+
 lemma [code]:
   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
   unfolding bex_triv_one_point1 ..
@@ -35,6 +39,8 @@
 definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   "filter_set P xs = {x\<in>xs. P x}"
 
+declare filter_set_def[symmetric, code unfold] 
+
 
 subsection {* Operations on lists *}
 
@@ -269,5 +275,7 @@
   Ball ("{*Blall*}")
   Bex ("{*Blex*}")
   filter_set ("{*filter*}")
+  fold ("{* foldl *}")
+
 
 end