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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
