--- a/NEWS Fri May 07 16:49:08 2021 +0200
+++ b/NEWS Sun May 09 05:48:50 2021 +0000
@@ -94,8 +94,12 @@
* Lemma "permutes_induct" has been given stronger
hypotheses and named premises. INCOMPATIBILITY.
-* Combinator "Fun.swap" moved into separate theory "Transposition" in
-HOL-Combinatorics. INCOMPATIBILITY.
+* Theory "Transposition" in HOL-Combinatorics provides elementary
+swap operation "transpose".
+
+* Combinator "Fun.swap" resolved into a mere input abbreviation
+in separate theory "Transposition" in HOL-Combinatorics.
+INCOMPATIBILITY.
*** ML ***