changed precedence of big operators: now like any other function symbol
authornipkow
Mon Jan 28 16:29:11 2019 +0100 (9 months ago)
changeset 697467404f5b91e56
parent 69745 aec42cee2521
child 69747 2755c387f1e6
changed precedence of big operators: now like any other function symbol
NEWS
     1.1 --- a/NEWS	Mon Jan 28 10:27:47 2019 +0100
     1.2 +++ b/NEWS	Mon Jan 28 16:29:11 2019 +0100
     1.3 @@ -74,6 +74,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* the functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
     1.8 +(not the corresponding binding operators) now have the same precedence
     1.9 +as any other prefix function symbol.
    1.10 +
    1.11  * Slightly more conventional naming schema in structure Inductive.
    1.12  Minor INCOMPATIBILITY.
    1.13  
    1.14 @@ -2998,9 +3002,9 @@
    1.15  performance.
    1.16  
    1.17  * Property values in etc/symbols may contain spaces, if written with the
    1.18 -replacement character "␣" (Unicode point 0x2324). For example:
    1.19 -
    1.20 -    \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
    1.21 +replacement character "?" (Unicode point 0x2324). For example:
    1.22 +
    1.23 +    \<star>  code: 0x0022c6  group: operator  font: Deja?Vu?Sans?Mono
    1.24  
    1.25  * Java runtime environment for x86_64-windows allows to use larger heap
    1.26  space.