--- a/NEWS Mon Apr 25 17:37:36 2016 +0200
+++ b/NEWS Mon Apr 25 19:41:39 2016 +0200
@@ -61,7 +61,8 @@
* Command 'define' introduces a local (non-polymorphic) definition, with
optional abstraction over local parameters. The syntax resembles
-'obtain' and fits better into the Isar language than old 'def'.
+'definition' and 'obtain'. It fits better into the Isar language than
+old 'def', which is now a legacy feature.
* Command '\<proof>' is an alias for 'sorry', with different
typesetting. E.g. to produce proof holes in examples and documentation.