changed precedence of big operators: now like any other function symbol
authornipkow
Mon, 28 Jan 2019 16:29:11 +0100
changeset 69762 7404f5b91e56
parent 69761 aec42cee2521
child 69763 2755c387f1e6
changed precedence of big operators: now like any other function symbol
NEWS
--- a/NEWS	Mon Jan 28 10:27:47 2019 +0100
+++ b/NEWS	Mon Jan 28 16:29:11 2019 +0100
@@ -74,6 +74,10 @@
 
 *** HOL ***
 
+* the functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
+(not the corresponding binding operators) now have the same precedence
+as any other prefix function symbol.
+
 * Slightly more conventional naming schema in structure Inductive.
 Minor INCOMPATIBILITY.
 
@@ -2998,9 +3002,9 @@
 performance.
 
 * Property values in etc/symbols may contain spaces, if written with the
-replacement character "␣" (Unicode point 0x2324). For example:
-
-    \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
+replacement character "?" (Unicode point 0x2324). For example:
+
+    \<star>  code: 0x0022c6  group: operator  font: Deja?Vu?Sans?Mono
 
 * Java runtime environment for x86_64-windows allows to use larger heap
 space.