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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
