[isabelle-dev] White space in theory names

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Jun 12 20:59:26 CEST 2014

This is an offspring from

I do not recommend white space in theory names: over the years proper
naming conventions have been increasingly enforced for logical entities
like variable names etc.  The issue with theory names maybe just escaped
attention due to its almost extralogical nature.  Nevertheless tools
like the code generator choke on theory names with white space.  Hence I
would argue for strictification here.

the fact that the quotient package would cut a name at white space
borders nevertheless seems strange to me and would deserve an inspection.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140612/b4120a15/attachment.asc>

More information about the isabelle-dev mailing list