equal
deleted
inserted
replaced
96 end |
96 end |
97 |
97 |
98 syntax |
98 syntax |
99 "_insert_fset" :: "args => 'a fset" ("{|(_)|}") |
99 "_insert_fset" :: "args => 'a fset" ("{|(_)|}") |
100 |
100 |
|
101 syntax_consts |
|
102 "_insert_fset" == fcons |
|
103 |
101 translations |
104 translations |
102 "{|x, xs|}" == "CONST fcons x {|xs|}" |
105 "{|x, xs|}" == "CONST fcons x {|xs|}" |
103 "{|x|}" == "CONST fcons x {||}" |
106 "{|x|}" == "CONST fcons x {||}" |
104 |
107 |
105 lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs" |
108 lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs" |