[isabelle-dev] Semantics of hide (open)

[Florian Haftmann]

>> 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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130108/e636b7fa/attachment.sig>