[isabelle-dev] Semantics of hide (open)

[Florian Haftmann]

Hi all,

I have the situation that I want to define via primrec a function with
an existing popular name (append) but retain the commonplace accesses
append for List.append and append.simps for List.append.simps (see
attached theory for a contrieved example).  With the existing semantics
of hide (open), I cannot achieve the desired effect; either (with
(open)), append.simps remains shadowed, or (without (open)) I am not
able to access Thy.append.simps any longer.

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.

This refers to hg id 1ea90e8046dc.

Cheers,
	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: Hiding.thy
Type: application/x-extension-thy
Size: 748 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121228/cd98199f/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121228/cd98199f/attachment.asc>