--- a/NEWS Tue May 31 20:56:09 2022 +0200
+++ b/NEWS Sat Jun 04 15:43:34 2022 +0200
@@ -40,8 +40,12 @@
* Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
longer. INCOMPATIBILITY.
-* Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
- type class preorder.
+* Theory "HOL.Relation":
+ - Added lemmas asymp_less and asymp_greater to type class preorder.
+ - Added predicate reflp_on and redefined reflp to ab an abbreviation.
+ Lemma reflp_def is explicitly provided for backward compatibility
+ but its usage is discouraged. Minor INCOMPATIBILITY.
+ - Added lemmas reflp_onI and reflp_onD.
* Theory "HOL-Library.Multiset":
- Consolidated operation and fact names.