--- a/NEWS Wed Nov 23 09:54:53 2022 +0100
+++ b/NEWS Wed Nov 23 09:57:59 2022 +0100
@@ -31,8 +31,10 @@
explicitly provided for backward compatibility but their usage is
discouraged. Minor INCOMPATIBILITY.
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
+ preorder.irreflp_greater[simp] ~> irreflp_on_greater[simp]
+ preorder.irreflp_less[simp] ~> irreflp_on_less[simp]
+ reflp_equality[simp] ~> reflp_on_equality[simp]
total_on_singleton
- reflp_equality[simp] ~> reflp_on_equality[simp]
- Added lemmas.
antisym_if_asymp
antisymp_if_asymp