NEWS
authordesharna
Fri, 26 May 2023 10:34:39 +0200
changeset 78111 a6989a7d192a
parent 78110 776f6b85243f
child 78116 cc17e2f0f1fc
child 78117 7735645667f0
NEWS
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