NEWS
changeset 82251 8cf503824ccf
parent 82249 bdefffffd05f
child 82252 8a7620fe0e83
--- a/NEWS	Wed Mar 12 21:53:25 2025 +0100
+++ b/NEWS	Thu Mar 13 09:41:56 2025 +0100
@@ -26,6 +26,13 @@
       wf_on_lex_prod[intro]
       wfp_on_iff_wfp
 
+* Theory "HOL.Order_Relation":
+  - Added lemmas.
+      antisym_relation_of[simp]
+      asym_relation_of[simp]
+      sym_relation_of[simp]
+      trans_relation_of[simp]
+
 * Theory "HOL-Library.Multiset":
   - Renamed lemmas. Minor INCOMPATIBILITY.
       filter_image_mset ~> filter_mset_image_mset