On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
Operations like Simplifier.context, Simplifier.inherit_context should
help here. Once that is repaired, I will see if the warning can now be
made an error that is more explicit about the reasons.
I am certainly in favour of this. First, tool developers mainly react on
errors with test runs, but do not see the warnings. Secondly, users do
not know who to report those warnings and do not know if they are caused
by their scripts or the tools.
Historically, the weak warning was a necessity due to too many simprocs
still not working with the context.
Let's hope that it can be easily switched to an explicit error after so
many years now.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
