Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed notin_fset to not_fmember
authordesharna
Fri, 26 May 2023 10:34:32 +0200
changeset 78110 776f6b85243f
parent 78109 5c6db3d1b602
child 78111 a6989a7d192a
renamed notin_fset to not_fmember
src/HOL/Library/FSet.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle