[isabelle-dev] Locale interpretation with mixins

[Florian Haftmann]

Hi Clemens, hi Makarius,

(sorry for being so little reactive on this imminent thread, but it
requires considerable preheating to catch the critical points)

> In December 2011 we were both staring at interpretation_with_defs.ML and
> could not fully see the principle how it would work for complex
> hiearchies of locales and interpretations.  I.e. it is EXPERIMENTAL with
> the capitalization that you've put there in Jan 2011 (c34415351b6d).

The issue is that I don't argue (or even propose) to integrate it into
the locale hierarchy, it should just remain on the outermost level,
interpretation from locales to theories.

> Just a general question: Why does the code generator require a closed
> constant as a starting point?  Couldn't it just take an arbitrary term,
> with some decoration how it should be abstracted into a closed thing?

Well, it can accomplish anything you tell it to do (cf.
http://dilbert.com/strips/comic/2006-01-29/).  But the idea has always
been to rely as closely as possible on the foundation without doing more
extralogical things than necessary.

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: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120906/79c72a06/attachment-0001.asc>