--- a/src/HOL/BNF/More_BNFs.thy Thu Mar 07 18:14:30 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy Fri Mar 08 09:34:38 2013 +0100
@@ -470,6 +470,8 @@
unfolding fset_rel_def fset_rel_aux by simp
qed auto
+lemmas [simp] = fset.map_comp' fset.map_id' fset.set_natural'
+
lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
unfolding fset_rel_def set_rel_def by auto
--- a/src/HOL/Quotient_Examples/FSet.thy Thu Mar 07 18:14:30 2013 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy Fri Mar 08 09:34:38 2013 +0100
@@ -722,6 +722,9 @@
shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T"
by (descending) (simp)
+lemma in_fset_map_fset[simp]: "a |\<in>| map_fset f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
+ by descending auto
+
subsection {* card_fset *}