--- a/src/HOL/Library/FSet.thy Wed May 17 09:00:04 2023 +0200
+++ b/src/HOL/Library/FSet.thy Fri May 26 09:48:55 2023 +0200
@@ -171,10 +171,10 @@
"{|x|}" == "CONST finsert x {||}"
abbreviation fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) where
- "a |\<in>| A \<equiv> a \<in> fset A"
+ "x |\<in>| X \<equiv> x \<in> fset X"
abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
- "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
+ "x |\<notin>| X \<equiv> x \<notin> fset X"
context includes lifting_syntax
begin