I have now committed these changes.
Clemens
On 28 October, 2015 21:53 CET, "Clemens Ballarin" <balla...@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-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
