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