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

[Makarius]

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

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

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


This refer to Isabelle/c7b7bca8592c.  The NEWS are just a (partial) 
summary of various renovations concerning explicit instantiations, which 
are ultimately motivated by the ongoing efforts to make Eisbach work with 
the coming release.  The main technical challenge of Eisbach is to have 
everything conform to certain Isar context disciplines, e.g. attributes 
"of", "where", and the notoriously outdated "rule_tac" family, which is 
now close to proper civilization.

There are no real incompatibilities with old uses, except for the default 
rule_insts_schematic = false as explained above.  I did not have the 
ambition to disable this legacy mode just now, but the complete conversion 
in AFP/aa0bd0c0cbb6 turned out rather small, indicating rare use of such 
undeclared schematic variables in rule_tac etc.


 	Makarius