--- 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.