NEWS
changeset 59849 c3d126c7944f
parent 59835 97872c658a44
child 59868 b1cd0c962780
child 59891 9ce697050455
--- a/NEWS	Sun Mar 29 23:08:03 2015 +0200
+++ b/NEWS	Mon Mar 30 00:13:37 2015 +0200
@@ -74,11 +74,6 @@
 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
-behaviour is still the default for some time.
-
 * Command "class_deps" takes optional sort arguments constraining
 the search space.