[isabelle-dev] Code export to Haskell and lower-case theory names
breitner at kit.edu
Fri Mar 29 18:40:17 CET 2013
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
Greetings and happy easter to those who care,
Dipl.-Math. Dipl.-Inform. Joachim Breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: This is a digitally signed message part
More information about the isabelle-dev