# HG changeset patch # User desharna # Date 1743586000 -7200 # Node ID b3b8c278af235918aa2d329f5a889bda3ee44542 # Parent ae2af2e085fdf5d25a26d0c7c991d9a807611dd6 tuned NEWS diff -r ae2af2e085fd -r b3b8c278af23 NEWS --- 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)