--- a/NEWS Sun Mar 29 16:01:12 2015 +0200
+++ b/NEWS Sun Mar 29 16:22:35 2015 +0200
@@ -61,15 +61,19 @@
*** 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".
-
* Explicit instantiation via attributes "where", "of", and proof methods
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
("_") that stand for anonymous local variables.
+* 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".
+Configuration option rule_insts_schematic (default false) controls use
+of schematic variables outside the context. Minor INCOMPATIBILITY,
+declare rule_insts_schematic = true temporarily and update to use local
+variable declarations or dummy patterns instead.
+
* 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