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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
