[isabelle-dev] Name for derived quotient_def theorem

[Florian Haftmann]

Hi Ondřej,

	in

http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53

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,
	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: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120328/119ec0d9/attachment.asc>