[isabelle-dev] White space in theory names

[Florian Haftmann]

This is an offspring from
http://fa.isabelle.narkive.com/QI1dxXvo/isabelle-quotient-type-command-fails

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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>