[isabelle-dev] NEWS: proper Isar context for rule instantiations
makarius at sketis.net
Mon Mar 30 00:16:41 CEST 2015
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.
More information about the isabelle-dev