In addition to Makarius' recent performance improvements, there is a modest reform to the way rewrite morphism are integrated with locales. Previously they were added as an after-thought to the interpretation commands. Now they are integrated with locale expressions.

The main advantage is that situations where locale expressions lead to duplicate constant declaration errors can now better be avoided. In principle, rewrite morphisms could also be allowed in locale declarations. This would imply a proof block after every locale declaration, so I haven't done so.

These are the relevant NEWS entries:

* Rewrites clauses (keyword 'rewrites') were moved into the locale
expression syntax, where they are part of locale instances.  In
interpretation commands rewrites clauses now need to occur before
'for' and 'defines'.  Minor INCOMPATIBILITY.

* For rewrites clauses, if activating a locale instance fails, fall
back to reading the clause first.  This helps avoid qualification of
locale instances where the qualifier's sole purpose is avoiding
duplicate constant declarations.

These are the relevant changesets in Isabelle and the AFP:
  Proper rewrite morphisms in locale instances.
Fall back to reading rewrite morphism first if activation fails without it.
  Drop rewrites after defines in interpretations.
  Rewrites clauses are now part of locale expressions.
  Pull rewrites clause in front of defines.

Some internal cleanup is still to come.

isabelle-dev mailing list

Reply via email to