1.1 --- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Mar 13 13:23:16 2013 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Mar 13 14:33:15 2013 +0100
     1.3 @@ -93,18 +93,23 @@
     1.4    "{|x, xs|}" == "CONST fcons x {|xs|}"
     1.5    "{|x|}"     == "CONST fcons x {||}"
     1.6  
     1.7 -lift_definition fset_member :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs"
     1.8 -   by simp
     1.9 +lemma member_transfer:
    1.10 +  assumes [transfer_rule]: "bi_unique A"
    1.11 +  shows "(A ===> list_all2 A ===> op=) (\<lambda>x xs. x \<in> set xs) (\<lambda>x xs. x \<in> set xs)"
    1.12 +by transfer_prover
    1.13 +
    1.14 +lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs"
    1.15 +   parametric member_transfer by simp
    1.16  
    1.17  abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
    1.18    "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
    1.19  
    1.20 -lemma fset_member_fmap[simp]: "a |\<in>| fmap f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
    1.21 +lemma fmember_fmap[simp]: "a |\<in>| fmap f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
    1.22    by transfer auto
    1.23  
    1.24  text {* We can export code: *}
    1.25  
    1.26 -export_code fnil fcons fappend fmap ffilter fset in SML
    1.27 +export_code fnil fcons fappend fmap ffilter fset fmember in SML
    1.28  
    1.29  subsection {* Using transfer with type @{text "fset"} *}
    1.30