NEWS

--- a/NEWS	Fri Jul 03 16:19:45 2015 +0200
+++ b/NEWS	Sun Jul 05 15:02:30 2015 +0200
@@ -234,6 +234,12 @@
 command. Minor INCOMPATIBILITY, use 'function' instead.
 
 
+** ML **
+
+* Thm.instantiate (and derivatives) no longer require the LHS of the
+instantiation to be certified: plain variables are given directly.
+
+
 
 New in Isabelle2015 (May 2015)
 ------------------------------