--- a/NEWS Mon Mar 22 00:07:55 2021 +0100
+++ b/NEWS Mon Mar 22 10:49:51 2021 +0000
@@ -65,8 +65,8 @@
specific "List_Permutation". Note that most notions from that
theory are already present in theory "Permutations". INCOMPATIBILITY.
-* Lemma "permutes_induct" has been given named premises.
-INCOMPATIBILITY.
+* Lemma "permutes_induct" has been given stronger
+hypotheses and named premises. INCOMPATIBILITY.
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
@@ -75,6 +75,9 @@
"order" are replaced or augmented by interpretations of locale
"ordering".
+* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor
+INCOMPATIBILITY; note that for most applications less elementary lemmas
+exists.
*** ML ***