--- a/NEWS Sun Mar 16 08:55:17 2025 +0100
+++ b/NEWS Sun Mar 16 14:51:37 2025 +0100
@@ -28,18 +28,23 @@
antisymp_equality[simp] ~> antisymp_on_equality[simp]
transp_equality[simp] ~> transp_on_equality[simp]
- Added lemmas.
+ antisym_on_bot[simp]
antisymp_on_bot[simp]
+ asym_on_bot[simp]
asymp_on_bot[simp]
+ irrefl_on_bot[simp]
irreflp_on_bot[simp]
left_unique_bot[simp]
left_unique_iff_Uniq
reflp_on_refl_on_eq[pred_set_conv]
+ sym_on_bot[simp]
symp_on_bot[simp]
symp_on_equality[simp]
totalp_on_mono[mono]
totalp_on_mono_strong
totalp_on_mono_stronger
totalp_on_mono_stronger_alt
+ trans_on_bot[simp]
transp_on_bot[simp]
* Theory "HOL.Wellfounded":