[isabelle-dev] Changes to the locale syntax
makarius at sketis.net
Fri Oct 30 17:20:01 CET 2015
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 "interpretation"
> and "interpret". In larger developments it is apparent that this is
> the better default.
When we introduced that difference of defaults around 2007, it was based
on a vague intuition about the most common uses in typical application.
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.
> * As already mentioned in my previous message, I plan to change the
> keyword for rewrite morphisms from "where" to "rewrites". This is to
> better distinguish these from named instantiations in locale
> expressions. The syntax will then be
> sublocale A < B where y = x for x rewrites "z = w"
> rather than
> sublocale A < B where y = x for x where "z = w"
Side remark: isabelle build -k helps to test hypotheses about feasibility
of new keywords. E.g.
isabelle build -d '$AFP' -k rewrites -n -a
No conflicts here.
More information about the isabelle-dev