[isabelle-dev] NEWS: More thorough check of proof context

[Makarius]

* More thorough check of proof context for goal statements and attributed 
fact expressions: background theory, declared hyps, declared variable 
names.  Potential INCOMPATIBILITY, tools need to observe standard 
context discipline.

This refers to Isabelle/f26a7f06266d.

It is a continuation of the thread by Dmitriy about not always reported 
errors seen in HOL-BNF 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-November/004833.html 
and one more step towards fully localized proof tools.


 	Makarius