--- a/NEWS Fri Apr 04 15:27:28 2025 +0200
+++ b/NEWS Wed Apr 02 11:26:40 2025 +0200
@@ -35,15 +35,15 @@
* 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
+ mono_on_invE
+ mono_on_strict_invE
monotone_on_inf_fun
monotone_on_sup_fun
+ strict_mono_on_eq
+ strict_mono_on_less
+ strict_mono_on_less_eq
- Removed lemmas. Minor INCOMPATIBILITY.
mono_on_greaterD (use mono_invE instead)