--- a/NEWS Sun Nov 20 23:53:39 2022 +0100
+++ b/NEWS Mon Nov 21 13:48:58 2022 +0100
@@ -27,24 +27,22 @@
* Theory "HOL.Relation":
- Strengthened lemmas. Minor INCOMPATIBILITY.
- preorder.reflp_ge
- preorder.reflp_le
total_on_singleton
- Added lemmas.
antisym_if_asymp
antisymp_if_asymp
irreflD
irreflpD
- linorder.totalp_ge[simp]
- linorder.totalp_greater[simp]
- linorder.totalp_le[simp]
- linorder.totalp_less[simp]
+ linorder.totalp_on_ge[simp]
+ linorder.totalp_on_greater[simp]
+ linorder.totalp_on_le[simp]
+ linorder.totalp_on_less[simp]
order.antisymp_ge[simp]
order.antisymp_le[simp]
preorder.antisymp_greater[simp]
preorder.antisymp_less[simp]
- preorder.reflp_ge[simp]
- preorder.reflp_le[simp]
+ preorder.reflp_on_ge[simp]
+ preorder.reflp_on_le[simp]
reflp_on_conversp[simp]
totalp_on_singleton[simp]