Quoting Makarius <makar...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
