[isabelle-dev] Changes to the locale syntax

[Clemens Ballarin]

I have now committed these changes.

Clemens


On 28 October, 2015 21:53 CET, "Clemens Ballarin" <ballarin at in.tum.de> 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.
> 
> * 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"
> 
> Clemens
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev