--- a/NEWS Tue Dec 13 11:29:52 2022 +0100
+++ b/NEWS Thu Dec 15 10:24:21 2022 +0100
@@ -30,6 +30,10 @@
irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are
explicitly provided for backward compatibility but their usage is
discouraged. Minor INCOMPATIBILITY.
+ - Added predicates antisym_on and antisymp_on and redefined antisym and
+ antisymp to be abbreviations. Lemmas antisym_def and antisymp_def are
+ explicitly provided for backward compatibility but their usage is
+ discouraged. Minor INCOMPATIBILITY.
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp]
preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]