[isabelle-dev] Changes to the locale syntax

[Florian Haftmann]

(continuing »Future of permanent_interpretation«)

> * 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.

Very fine.

> * 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"

Sounds good, and hints nicely towards »rewrite morphism«.

Concerning permanent_interpretation, I will consider using »defines«
instead of »defining« for consistency then.

I will come back to that implementation work soon – the integration of
the add-on »permanent interpretation« into Pure is independent of any
conceptual thought for future keywords.  It will also make apparent how
mixin definitions appear as clever interweaving of existing mechanisms,
not touching the foundations of locales and locale expressions at all.

Cheers,
	Florian

(concluding some mails scattered over various threads).

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151029/ed130dc4/attachment.sig>