Hi Ondřej,
inhttp://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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
