NEWS

--- a/NEWS	Tue Jun 09 16:42:17 2015 +0200
+++ b/NEWS	Tue Jun 09 22:24:33 2015 +0200
@@ -12,6 +12,9 @@
 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
 proof body as well, abstracted over relevant parameters.
 
+* Term abbreviations via 'is' patterns also work for schematic
+statements: result is abstracted over unknowns.
+
 * Local goal statements (commands 'have', 'show', 'hence', 'thus') allow
 an optional context of local variables ('for' declaration).