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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
