[isabelle-dev] Semantics of hide (open)
florian.haftmann at informatik.tu-muenchen.de
Tue Jan 8 20:32:30 CET 2013
>> Maybe there is some confusion what the semantics of hide (open) is
>> exactly supposed to be. But since the current state of affairs gives
>> no tool at hand to resolve situations as sketched above, this is a
>> serious obstacle.
> The "hide" feature was added as a temporary workaround for the lack of
> proper scope management many years ago. In the meantime we managed to
> get a bit further with the "naming + binding = name + accesses"
> equation, but not with scoping of theories and contexts. I still would
> like to see that appear eventually, and "hide" become obsolete then.
> (It will mean that names behave uniformly, i.e. different categories
> like "const" and "fact" need to agree in their visibility.)
That indeed would be the right thing. In the meantime I found out that
I do not need function/primrec anywayin my particular situation, so the
»serious obstacle« has disappeared.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev