[isabelle-dev] Changes to the locale syntax

[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 "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.


 	Makarius