NEWS

--- a/NEWS	Sun Apr 24 20:37:24 2016 +0200
+++ b/NEWS	Sun Apr 24 21:31:14 2016 +0200
@@ -59,6 +59,10 @@
 
 *** Isar ***
 
+* 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'.
+
 * Command '\<proof>' is an alias for 'sorry', with different
 typesetting. E.g. to produce proof holes in examples and documentation.