Re: [isabelle-dev] Future of permanent_interpretation

Hi Florian, I looked at the documentation generated with this patch, and the first impression of the "Locale interpretation" section is that it now looks funny -- probably due to the transitional nature of the patch. For "interpretation" there are now two declarations and two productions,

Re: [isabelle-dev] Future of permanent_interpretation

For further discussion, see now fd4ac1530d63, particulary src/Pure/Isar/interpretation.ML and 5.7.3 »Locale interpretation« in *isar-ref*. This goes along the following lines: * »Interpretation« in general is used as generic heading for every kind of intepretation into different destination

Re: [isabelle-dev] Future of permanent_interpretation

> What is the conclusion of this thread for the coming release? Whatever > happens, the time window for it is approx. Nov/Dec 2015. The situation is still somehow inconclusive. I am working currently to re-integrate permanent_interpretation »as it is« into Pure, to provide a base for further

Re: [isabelle-dev] Future of permanent_interpretation

On 09 November, 2015 11:56 CET, Makarius wrote: > It is formally trivial to have 'permanent_interpretation' in Isabelle/Pure > as separate command. If there is a simple way to have just one > 'interpretation' command with 'defines' vs. 'rewrites', I would prefer >

Re: [isabelle-dev] Future of permanent_interpretation

What is the conclusion of this thread for the coming release? Whatever happens, the time window for it is approx. Nov/Dec 2015. Historically, the 'permanent_interpretation' command had to stay outside Isabelle/Pure and Main Isabelle/HOL, because it was overwriting the 'interpretation' command

Re: [isabelle-dev] Future of permanent_interpretation

Hi Florian, thanks for your feedback. Local theories have done Isabelle and its users a great service in presenting a uniform view of different kinds of declarations in several contexts, and the locales reimplementation would have been much more painful without them. However, if "local

Re: [isabelle-dev] Future of permanent_interpretation

On 28/10/2015 21:41, Clemens Ballarin wrote: On 26 October, 2015 10:38 CET, Tobias Nipkow wrote: My desire to generate code from locale interpretations w/o having to make a number of trivial function definitions was what started this whole business a number of years back.

Re: [isabelle-dev] Future of permanent_interpretation

Hi Clemens et al., let me put things in a broader perspective. I think we have two views on the whole machinery: * The algebraic view with locales, sublocale statements and (somehow global) interpretation statements. This view is important because it essentially describes the implementation of

Re: [isabelle-dev] Future of permanent_interpretation

(this continues the previous mail) Certainly, your work has partly been inspired by the feeling that the current locale commands only provide the bare basics for manipulating locales. For example, basing an interpretation or sublocale declaration on definitions is certainly

Re: [isabelle-dev] Future of permanent_interpretation

I am very happy to see that we agree that a "defines" section is a useful addition to the interpretation command. But at the moment, this section only exists for "permanent_interpretation". It would be nice if "interpretation" were enhanced with "defines", in which case people could make use

Re: [isabelle-dev] Future of permanent_interpretation

On 26 October, 2015 10:38 CET, Tobias Nipkow wrote: > My desire to generate code from locale interpretations w/o having to make a > number of trivial function definitions was what started this whole business a > number of years back. Florian's very useful implementation of

[isabelle-dev] Future of permanent_interpretation

Recently in private discussion there was the question what the supposed future of permanent_interpretation is supposed to be. It looks as follows: Step 1) * Put »permanent_interpretation« into Pure directly. Step 2) * Careful revisiting of the documentation to emphasize the