--- a/NEWS Tue Aug 29 20:34:43 2017 +0100
+++ b/NEWS Wed Aug 30 18:01:27 2017 +0200
@@ -250,6 +250,8 @@
* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
for pattern aliases as known from Haskell, Scala and ML.
+* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.
+
* Session HOL-Analysis: more material involving arcs, paths, covering
spaces, innessential maps, retracts, material on infinite products.
Major results include the Jordan Curve Theorem and the Great Picard