# HG changeset patch
# User desharna
# Date 1685090079 -7200
# Node ID a6989a7d192af9b018a13bc49ed6fee68359bdb7
# Parent  776f6b85243f5ed58363c617c00ebb3e3e7eabf4
NEWS

diff -r 776f6b85243f -r a6989a7d192a NEWS
--- a/NEWS	Fri May 26 10:34:32 2023 +0200
+++ b/NEWS	Fri May 26 10:34:39 2023 +0200
@@ -219,6 +219,13 @@
       wf_if_convertible_to_wf
 
 * Theory "HOL-Library.FSet":
+  - Redefined fmember as an abbreviation based on Set.member.
+    Minor INCOMPATIBILITY.
+  - Redefined notin_fset as an abbreviation based on Set.not_member and
+    renamed to not_fmember. Minor INCOMPATIBILITY.
+  - Removed lemmas. Minor INCOMPATIBILITIES.
+      fmember_iff_member_fset
+      notin_fset
   - Added lemmas.
       fimage_strict_mono
       wfP_pfsubset