--- a/NEWS Sun Sep 18 21:06:24 2016 +0200
+++ b/NEWS Mon Sep 19 12:53:30 2016 +0200
@@ -236,7 +236,7 @@
iterated quantification \<exists>!x y. P x y with its slightly confusing
sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
-(analogous existing notation \<exists>!(x, y)\<in>A. P x y). Potential
+(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential
INCOMPATIBILITY in rare situations.
* Renamed session HOL-Multivariate_Analysis to HOL-Analysis.