# HG changeset patch
# User wenzelm
# Date 1427149000 -3600
# Node ID f19f4afa49e289f07dd98354af7983be46b5c94d
# Parent  d9765e17947f144f2cd21895ab4ebb19b1946933
NEWS;

diff -r d9765e17947f -r f19f4afa49e2 NEWS
--- a/NEWS	Mon Mar 23 23:12:33 2015 +0100
+++ b/NEWS	Mon Mar 23 23:16:40 2015 +0100
@@ -61,6 +61,11 @@
 
 *** Pure ***
 
+* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
+etc.) allow an optional context of local variables ('for' declaration):
+these variables become schematic in the instantiated theorem. This
+behaviour is analogous to 'for' in attributes "where" and "of".
+
 * Command "class_deps" takes optional sort arguments constraining
 the search space.