[isabelle-dev] Name for derived quotient_def theorem

[Makarius]

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.


 	Makarius