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

Makarius makarius at sketis.net
Mon Jan 13 17:01:25 CET 2014

* 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 
and one more step towards fully localized proof tools.


More information about the isabelle-dev mailing list