# HG changeset patch
# User desharna
# Date 1685090072 -7200
# Node ID 776f6b85243f5ed58363c617c00ebb3e3e7eabf4
# Parent  5c6db3d1b6026231353e6abb2b94333684fa0a9e
renamed notin_fset to not_fmember

diff -r 5c6db3d1b602 -r 776f6b85243f src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri May 26 09:59:06 2023 +0200
+++ b/src/HOL/Library/FSet.thy	Fri May 26 10:34:32 2023 +0200
@@ -174,7 +174,7 @@
 abbreviation fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) where
   "x |\<in>| X \<equiv> x \<in> fset X"
 
-abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
+abbreviation not_fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
   "x |\<notin>| X \<equiv> x \<notin> fset X"
 
 context includes lifting_syntax