[isabelle-dev] Name for derived quotient_def theorem
makarius at sketis.net
Wed Mar 28 17:12:47 CEST 2012
On Wed, 28 Mar 2012, Ondřej Kunčar wrote:
> After a long discussion during a lunch break we decided to use
> ".rep_eq". I will also change "_rsp" to ".rsp". What about "_def"?
> Should I change it to ".def" as well? "_def" seems to be a
> inconsistency, I guess because of historical reasons. Should new
> packages use ".def" instead of "_def"?
I don't see a reason for ".def" -- the traditional "_def" still does its
job. By convention it somehow refers to a basic definition behind the
scenes, which is sometimes public, sometimes considered private.
BTW, qualified bindings do work in general, but not for term entities.
So a Local_Theory.define with qualified names will not exactly work as
could be expected, although that is its normal hevaiour: to regard only
the base name in the auxiliary context. So local term definitions of some
"foo.make" and "bar.make" will cause an error.
More information about the isabelle-dev