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
