florian.haftmann at informatik.tu-muenchen.de
Wed Apr 18 20:06:38 CEST 2012
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev