src/HOL/Quotient_Examples/FSet.thy

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