NEWS

--- a/NEWS	Mon Jun 08 14:45:31 2015 +0200
+++ b/NEWS	Mon Jun 08 19:38:08 2015 +0200
@@ -9,6 +9,9 @@
 
 *** Pure ***
 
+* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
+the proof body as well, abstracted over hypothetical parameters.
+
 * New Isar command 'supply' supports fact definitions during goal
 refinement ('apply' scripts).