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