Re: [isabelle-dev] Changes to the locale syntax

2015-11-14 Thread Makarius
On Fri, 30 Oct 2015, Makarius wrote: I don't mind to change that, and thus make it more uniform. It is mainly a matter of the empirical situation found in the visible universe of Isabelle examples + AFP if it is feasible / desirable. To conclude this thread, here are more changes to push it

Re: [isabelle-dev] Changes to the locale syntax

2015-11-04 Thread Clemens Ballarin
I have now committed these changes. Clemens On 28 October, 2015 21:53 CET, "Clemens Ballarin" wrote: > I'm planning two moderate changes to the locale syntax: > > * The default of qualifiers in locale expressions will change from optional > ("?") to mandatory ("!") in

Re: [isabelle-dev] Changes to the locale syntax

2015-10-30 Thread Makarius
On Wed, 28 Oct 2015, Clemens Ballarin wrote: 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

Re: [isabelle-dev] Changes to the locale syntax

2015-10-29 Thread Florian Haftmann
(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

[isabelle-dev] Changes to the locale syntax

2015-10-28 Thread Clemens Ballarin
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