[isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]
florian.haftmann at informatik.tu-muenchen.de
Tue Dec 29 08:48:51 CET 2015
> 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
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
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,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev