[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

Makarius makarius at sketis.net
Fri Oct 19 16:35:58 CEST 2012

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.


More information about the isabelle-dev mailing list