[isabelle-dev] Changes to the locale syntax

I'm planning two moderate changes to the locale syntax: * 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

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