[isabelle-dev] NEWS: Locale rewrite morphism moved into expressions

[Clemens Ballarin]

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:

http://isabelle.in.tum.de/repos/isabelle/rev/b6ce18784872
   Proper rewrite morphisms in locale instances.
http://isabelle.in.tum.de/repos/isabelle/rev/d5a7f2c54655
   Fall back to reading rewrite morphism first if activation fails 
without it.
http://isabelle.in.tum.de/repos/isabelle/rev/0f8cb5568b63
   Drop rewrites after defines in interpretations.

https://bitbucket.org/isa-afp/afp-devel/commits/744680a5363124dad21569ea3fdc431d5aad2e00
   Rewrites clauses are now part of locale expressions.
https://bitbucket.org/isa-afp/afp-devel/commits/6bfd6925be04049bc9d0833708ae42685a3ac6b9
   Pull rewrites clause in front of defines.

Some internal cleanup is still to come.

Clemens