--- a/NEWS Mon Jun 20 11:06:33 2022 +0200
+++ b/NEWS Tue Jun 21 13:39:06 2022 +0200
@@ -40,8 +40,16 @@
* Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
longer. INCOMPATIBILITY.
+* Theory "HOL.Fun":
+ - Added predicate monotone_on and redefined monotone to be an
+ abbreviation. Lemma monotone_def is explicitly provided for backward
+ compatibility but its usage is discouraged. Minor INCOMPATIBILITY.
+ - Added lemmas.
+ monotone_onD
+ monotone_onI
+
* Theory "HOL.Relation":
- - Added predicate reflp_on and redefined reflp to ab an abbreviation.
+ - Added predicate reflp_on and redefined reflp to be an abbreviation.
Lemma reflp_def is explicitly provided for backward compatibility
but its usage is discouraged. Minor INCOMPATIBILITY.
- Added predicate totalp_on and abbreviation totalp.