[isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]
ballarin at in.tum.de
Sun Apr 7 12:59:42 CEST 2013
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
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
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.
More information about the isabelle-dev