[isabelle-dev] copy_bnf

Dear Dmitriy, I like the new "copy_bnf" command a lot, especially to allow records to be used in nested recursion. However, after a record definition, I have to invoke the command manually*. I would like to propose that "record" gains an option to call it directly. So, instead of writing:

Re: [isabelle-dev] copy_bnf

Hi Lars, this was exactly the vision for copy_bnf, modulo that I thought of using a plugin (“src/Pure/Tools/plugin.ML”) instead of an option. But since I am not the author of record, I went for the less invasive option of a separate command (in the spirit of setup_lifting for typedef). So if

Re: [isabelle-dev] copy_bnf

> I guess the general question is, whether it is fine to add the plugin > infrastructure for (most of the) existing commands (e.g., definition, > typedef, record, fun), thus enabling us writing tools that extend the > command’s functionality (be them enabled by default or not). I am

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

»const_decl« is shared by different primitives and operations on various targets. Hence the patch looks fine. The »revert_abbrev« goes back to changeset 2b86fac03ec5 in named_target.ML, although the guarding criterion has changed over time. 2b86fac03ec5 is already in the highly experimental

Re: [isabelle-dev] code abbreviation for mapping over a fixed range

Hi Christian, > This email refers to the following commit: > > http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251 > > code abbreviation for mapping over a fixed range > > Is there a specific reason for this code equation: > > "map_range f (Suc n) = map_range f n @ [f n]" > > It

Re: [isabelle-dev] Explicit option "open" for code_reflect

Hi Frédéric, > For a few number of constants it should be possible to write all > constants by hand. For a large number, I will see how feasible it is to > generate this list of constants, or find otherwise a simpler solution... code_reflect is definitely not intended as a watering bin. The

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] [isabelle] Contracting Abbreviations of Locale Definitions

Hi Clemens, thanks for undertaking this. I will have a look at this and give feedback. Cheers, Florian Am 27.10.2015 um 18:59 schrieb Clemens Ballarin: > Related to the below discussion on isabelle-users, I have now refined the > patch I had circulated then. Here is the NEWS entry: >

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] Changes to the locale syntax

(continuing »Future of permanent_interpretation«) > * The default of qualifiers in locale expressions will change from optional ("?") to mandatory ("!") in the context of "locale" and "sublocale". This brings these commands in line with "interpretation" and "interpret". In larger developments

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