NEWS
changeset 61701 e89cfc004f18
parent 61694 6571c78c9667
child 61729 30d4ccd54861
     1.1 --- a/NEWS	Wed Nov 18 17:37:00 2015 +0000
     1.2 +++ b/NEWS	Wed Nov 18 21:18:33 2015 +0100
     1.3 @@ -314,6 +314,28 @@
     1.4  * Keyword 'rewrites' identifies rewrite morphisms in interpretation
     1.5  commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY.
     1.6  
     1.7 +* More gentle suppression of syntax along locale morphisms while
     1.8 +printing terms.  Previously 'abbreviation' and 'notation' declarations
     1.9 +would be suppressed for morphisms except term identity.  Now
    1.10 +'abbreviation' is also kept for morphims that only change the involved
    1.11 +parameters, and only 'notation' is suppressed.  This can be of great
    1.12 +help when working with complex locale hierarchies, because proof
    1.13 +states are displayed much more succinctly.  It also means that only
    1.14 +notation needs to be redeclared if desired, as illustrated by this
    1.15 +example:
    1.16 +
    1.17 +  locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)
    1.18 +  begin
    1.19 +    definition derived (infixl "\<odot>" 65) where ...
    1.20 +  end
    1.21 +
    1.22 +  locale morphism =
    1.23 +    left: struct composition + right: struct composition'
    1.24 +    for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)
    1.25 +  begin
    1.26 +    notation right.derived ("\<odot>''")
    1.27 +  end
    1.28 +
    1.29  * Command 'sublocale' accepts mixin definitions after keyword
    1.30  'defines'.
    1.31