NEWS
changeset 67119 acb0807ddb56
parent 67099 3345d53e7c58
child 67133 540eeaf88a63
     1.1 --- a/NEWS	Sat Dec 02 16:50:53 2017 +0000
     1.2 +++ b/NEWS	Sun Dec 03 13:22:09 2017 +0100
     1.3 @@ -9,6 +9,10 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* The old 'def' command has been discontinued (legacy since
     1.8 +Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
     1.9 +object-logic equality or equivalence.
    1.10 +
    1.11  * Session-qualified theory names are mandatory: it is no longer possible
    1.12  to refer to unqualified theories from the parent session.
    1.13  INCOMPATIBILITY for old developments that have not been updated to