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

Joachim Breitner breitner at kit.edu
Tue Apr 2 12:38:17 CEST 2013


Am Dienstag, den 02.04.2013, 12:31 +0200 schrieb Makarius:
> So far there were no reasons given on this thread why the convention 
> should not be followed first place.  Are there any?

ignorance? I was using Isabelle for quite a while before I heard about
these conventions, and even longer before I learned that not following
them can cause severe issues.

As I said: If it can cause issues beyond inconvenience (and you say it
can), then the convention should become the rule and enforced by the
system, to prevent users from accidentally not following the rule.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
-------------- 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/20130402/04f5e417/attachment.sig>

More information about the isabelle-dev mailing list