--- a/NEWS Mon Mar 31 10:15:48 2025 +0200
+++ b/NEWS Mon Mar 31 22:46:11 2025 +0100
@@ -35,10 +35,17 @@
* Theory "HOL.Fun":
- Added lemmas.
+ mono_on_strict_invE
+ mono_on_invE
+ strict_mono_on_eq
+ strict_mono_on_less_eq
+ strict_mono_on_less
antimonotone_on_inf_fun
antimonotone_on_sup_fun
monotone_on_inf_fun
monotone_on_sup_fun
+ - Removed lemmas. Minor INCOMPATIBILITY.
+ mono_on_greaterD (use mono_invE instead)
* Theory "HOL.Relation":
- Changed definition of predicate refl_on to not constrain the domain