[isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]

[Florian Haftmann]

Hi Clemens,

> I didn't have time to look at your patches, and since I only have
superficial knowledge of instantiation contexts I didn't fully
understand the example either.  I guess though that the purpose of these
global interpretations is to propagate some constant declarations into
the surrounding theory.  If this is useful we should certainly have such
a command.

thanks for looking into that.

> What I still fail to understand is why you want to use 'global_interpretation'
as keyword if the command occurs directly in a theory.  This is
redundant.  I now take this as a temporary solution until there is some
better terminology for distinguishing kinds of interpretations, and I
very much hope that we will not get into another debate about renaming
'interpretation' to 'global_interpretation' or similar after the 2016
release.

I am personally very comfortable with the situation »as it is« by now
and I am convinced there is now much time to breathe before we have to
make any final decisions on that matter.

Enjoy your time,
	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: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151229/6bb69156/attachment.sig>