* 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
