[isabelle-dev] HOL/ex/Set_Algebras

[Florian Haftmann]

Hi Clemens,

>> 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«.
> 
> This looks to me like a special case, but maybe one that is encountered
> frequently when generating code.  What do you intend to do?  Provide a
> special version of interpretation for code generation?

the intension is:

def (in foo) bar where …
  --[ interpretation foo: … ]-->
    def (in -) bar where …

rather than

def (in foo) bar where …
  --[ interpretation foo: … ]-->
    abbreviation (in -) bar where …

with --[ … ]--> being the interpretation morphism.  The interpretation +
defines pattern was something which could be accomplished rather simple,
so I decided to make an experimental start with this in December 2010.

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/20120419/351b0da7/attachment.sig>