[isabelle-dev] Name for derived quotient_def theorem

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Mar 28 07:26:44 CEST 2012

Hi Ondřej,



the name given to the derived theorem is unsatisfactory.  Since it is
not a »code-only« theorem, it should not carry the »code« within.  If it
would be a »code-only« theorem, the convention is to suffix with
»_code«, not »_code_eqn«.

Also, for derived theorems proved by packages it is much more common to
use qualification suffixes (e.g. ».simp«, ».intro«) rather than plumbing
underscores (cf. module binding.ML).  Btw. this also applies to the
respectfulness theorem: ».rsp« would be better than »_rsp«.

What about ».simp«?

All the best,


PGP available:

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

More information about the isabelle-dev mailing list