# HG changeset patch
# User wenzelm
# Date 1427277568 -3600
# Node ID 3b6ad54b04fc2c1a8388767da892447a9a85f9bd
# Parent  22bc39064290e9f55c27c04703644dbd3a3b30e5
NEWS;

diff -r 22bc39064290 -r 3b6ad54b04fc NEWS
--- a/NEWS	Wed Mar 25 10:44:57 2015 +0100
+++ b/NEWS	Wed Mar 25 10:59:28 2015 +0100
@@ -70,6 +70,11 @@
 "rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
 ("_") that stand for anonymous local variables.
 
+* Configuration option "rule_insts_schematic" determines whether proof
+methods like "rule_tac" may refer to undeclared schematic variables
+implicitly, instead of using proper 'for' declarations.  This historic
+behaviour is still the default for some time.
+
 * Command "class_deps" takes optional sort arguments constraining
 the search space.