--- 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