Hi Clemens, > If you follow up the imported theory, you will find some code that > provides a clone of the interpretation command (under the same name!) > with some added functionality (definitions).
> Its purpose
> might have been to make the interpretation notationally simpler.
the story behind is not about syntax. It is really about the
simultaneous definitions. For a motivation, you can have a look at the
tutorial on code generation, section »Further issues«, »Locales and
interpretation«, where the pattern behind interpretation plus definition
is spelt out using the constant »funpows«.
I have this clone on my todo list, actually the leading point on my
after-release todo list, and hope to be able to get rid of it, but I
have to study mixins before in depth.
Cheers,
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
