[isabelle-dev] Locale interpretation with mixins
florian.haftmann at informatik.tu-muenchen.de
Thu Sep 6 10:55:58 CEST 2012
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 259 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev