Re: [isabelle] Simplifier: renamed bound variable ":000" to ":000a"

On Wed, 17 Feb 2010, Brian Huffman wrote:

If I understand you correctly, the "renamed bound variable" message indicates a problem in the *implementation* of some part of the simplifier. So the message is only potentially useful to developers, and not ordinary users.

No, it indicates that the Simplifier has just repaired a problem introduced in user space, notably one of these Simplifier plugins that can be defined in the library. Since the main library in question is actually main HOL, one could nonetheless argue that it is somehow relevant to developers.

I would like Isabelle to refrain from printing warning messages unless they provide meaningful information that users can act upon.

I am usually trying hard to keep messages relevant, and fight spam wherever possible, although this often seems futile. As messages are cleaned up here, new ones emerge there.

Concerning this particular message, I would not just switch it of because it is an important reminder that certain things in HOL still need to be sorted out. Maybe you can help looking through all the simprocs ...


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.