| changeset 82392 | b161057bdd41 |
| parent 82390 | 558bff66be22 |
| child 82398 | b3b8c278af23 |
--- a/NEWS Mon Mar 31 22:46:18 2025 +0100 +++ b/NEWS Tue Apr 01 10:20:14 2025 +0200 @@ -36,10 +36,10 @@ * 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 + 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