--- a/NEWS Thu Aug 23 17:09:37 2018 +0000
+++ b/NEWS Thu Aug 23 17:09:39 2018 +0000
@@ -14,6 +14,15 @@
specified in seconds; a negative value means it is disabled (default).
+*** HOL ***
+
+* Simplified syntax setup for big operators under image. In rare
+situations, type conversions are not inserted implicitly any longer
+and need to be given explicitly. Auxiliary abbreviations INFIMUM,
+SUPREMUM, UNION, INTER should now rarely occur in output and are just
+retained as migration auxiliary. INCOMPATIBILITY.
+
+
New in Isabelle2018 (August 2018)
---------------------------------