[isabelle-dev] NEWS: proper Isar context for rule instantiations

[Makarius]

On Sun, 29 Mar 2015, Makarius wrote:

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

This part is actually old NEWS, and removed in Isabelle/c3d126c7944f.

For overly conservative users, the default of rule_insts_schematic = false 
might be the most relevant incompatibility.


 	Makarius