--- a/NEWS Sun Nov 05 16:57:03 2017 +0100
+++ b/NEWS Sun Nov 05 17:45:17 2017 +0100
@@ -14,6 +14,9 @@
INCOMPATIBILITY for old developments that have not been updated to
Isabelle2017 yet (using the "isabelle imports" tool).
+* Theory header 'abbrevs' specifications need to be separated by 'and'.
+INCOMPATIBILITY.
+
* Only the most fundamental theory names are global, usually the entry
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for