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

[Joachim Breitner]

Hi,

Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius:
> > This has got nothing to do with Isabelle's informal conventions but is 
> > all about the target language's formal rules.
> 
> The conventions about theory names and locale/class names are not that 
> informal.  If you violate them systematically, certain name space policies 
> will break down.  That is then a "general user error".

Are there really things that break if I deviate from the convention?
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).

Greetings and happy easter to those who care,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130329/8cd3c24d/attachment.sig>