Yes, "simps" should not be used for special purpose rules. Tobias
Am 28/03/2012 09:22, schrieb Lukas Bulwahn: > Hi Florian, > > > Thank you for your suggestions. We will take them into account. > > On 03/28/2012 07:26 AM, Florian Haftmann wrote: >> 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«. > > This is explained by looking at the history: The typedef package introduces > names with underscores, quotient_type and quotient_def inherit this from > typedef. > > Here a list of names we were thinking of while discussing: > > - abstract_eq > - abs_equation > - abs_def > - code_cert > - code_certificate > > In the end, we decided for the one you can see (although I am personally still > in favor of abs_equation or similar). > I think ".simp" is rather strange, because it is really not simplifying > anything, but rather unfolding the definition in some special way. > > > Lukas > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev