clarified NEWS (cf. 97872c658a44);
authorwenzelm
Mon, 30 Mar 2015 00:13:37 +0200
changeset 59849 c3d126c7944f
parent 59848 18c21d5c9138
child 59850 f339ff48a6ee
clarified NEWS (cf. 97872c658a44);
NEWS
--- 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.