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