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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
