NEWS

--- a/NEWS	Mon Mar 20 15:01:12 2023 +0100
+++ b/NEWS	Mon Mar 20 15:01:59 2023 +0100
@@ -66,6 +66,11 @@
 * Theory "HOL.Finite_Set"
   - Imported Relation instead of Product_Type, Sum_Type, and Fields.
     Minor INCOMPATIBILITY.
+  - Added lemmas.
+      Finite_Set.bex_max_element
+      Finite_Set.bex_min_element
+      is_max_element_in_set_iff
+      is_min_element_in_set_iff
 
 * Theory "HOL.Relation":
   - Imported Product_Type, Sum_Type, and Fields instead of Finite_Set.