[isabelle-dev] HOL/ex/Set_Algebras

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120418/8c9a9f25/attachment.sig>