diff -r 990c9fea6773 -r 12cc54fac9b0 NEWS
--- a/NEWS	Tue Jun 09 15:28:06 2015 +0200
+++ b/NEWS	Tue Jun 09 16:07:11 2015 +0200
@@ -7,14 +7,20 @@
 New in this Isabelle version
 ----------------------------
 
+*** Isar ***
+
+* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
+proof body as well, abstracted over relevant parameters.
+
+* Local goal statements (commands 'have', 'show', 'hence', 'thus') allow
+an optional context of local variables ('for' declaration).
+
+* New command 'supply' supports fact definitions during goal refinement
+('apply' scripts).
+
+
 *** Pure ***
 
-* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
-the proof body as well, abstracted over relevant parameters.
-
-* New Isar command 'supply' supports fact definitions during goal
-refinement ('apply' scripts).
-
 * Configuration option rule_insts_schematic has been discontinued
 (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.