[isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]

[Clemens Ballarin]

Quoting Makarius <makarius at sketis.net>:

> On Tue, 26 Mar 2013, Florian Haftmann wrote:
>
> Note that we have one more aspect in the back-end that could help  
> here: the 'private' modifier.

What would the 'private' modifier do in general?  This sounds like a  
new concept.

The following may or may not be related: I recently spent some thought  
on getting rid of the mandatory vs optional distinction of qualifiers.  
  In any case this will likely have considerable impact, so here's the  
idea:

Currently there is the strange feature that abbreviations are only  
unfolded under morphisms that are the identity on term parameters.   
 From what I see on the mailing lists this has confused users.   
Instead, I would propose to change the criterion to that abbreviations  
are only unfolded under morphisms that do not change the name part  
(i.e. without qualification).  This would mean that for an unqualified  
instance syntax remained available while for a qualified instance  
syntax redeclaration would be necessary.

This would, of course, require some experimentation, but for now I  
just would like to learn whether the 'private' modifier would be  
related and should be taken into consideration.

Clemens