[isabelle-dev] Code export to Haskell and lower-case theory names

[Makarius]

On Fri, 29 Mar 2013, Brian Huffman wrote:

>> Then it should be a hard rule enforced by the system. If that is not 
>> the case, then it should be fully supported and up to the user to 
>> choose his naming, even if it deviate from what others use (she might 
>> have reasons for that).
>
> I completely agree.

Enforcing rules in a strict manner is always a very painful process. 
We've done that over the years where it was absolutely necessary, e.g. 
making the theorem name space conform to the policies of any other name 
space (types, consts, etc.), despite all the complaints that were coming 
from it.  Now it is difficult to imagine that theorems would work 
otherwise.

Generally, I see a variety of levels of checking by the system, a spectrum 
between enforcement to encourgement: error, warning, hilighting. BTW, in 
Isabelle/jEdit a plain warning already looks quite prominent.


 	Makarius