--- a/NEWS Mon Mar 17 09:00:40 2025 +0100
+++ b/NEWS Mon Mar 17 09:12:18 2025 +0100
@@ -40,16 +40,24 @@
irreflp_on_bot[simp]
left_unique_bot[simp]
left_unique_iff_Uniq
+ refl_on_top[simp]
reflp_on_refl_on_eq[pred_set_conv]
+ reflp_on_top[simp]
sym_on_bot[simp]
+ sym_on_top[simp]
symp_on_bot[simp]
symp_on_equality[simp]
+ symp_on_top[simp]
+ total_on_top[simp]
totalp_on_mono[mono]
totalp_on_mono_strong
totalp_on_mono_stronger
totalp_on_mono_stronger_alt
+ totalp_on_top[simp]
trans_on_bot[simp]
+ trans_on_top[simp]
transp_on_bot[simp]
+ transp_on_top[simp]
* Theory "HOL.Wellfounded":
- Added lemmas.