NEWS

--- a/NEWS	Sat Dec 02 16:50:53 2017 +0000
+++ b/NEWS	Sun Dec 03 13:22:09 2017 +0100
@@ -9,6 +9,10 @@
 
 *** General ***
 
+* The old 'def' command has been discontinued (legacy since
+Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
+object-logic equality or equivalence.
+
 * Session-qualified theory names are mandatory: it is no longer possible
 to refer to unqualified theories from the parent session.
 INCOMPATIBILITY for old developments that have not been updated to