tuned;
authorwenzelm
Tue May 28 19:52:14 2019 +0200 (7 weeks ago)
changeset 7029767edf0234417
parent 70293 c7e9d3a0a681
child 70298 ad2d84c42380
tuned;
NEWS
     1.1 --- a/NEWS	Mon May 27 15:08:51 2019 +0200
     1.2 +++ b/NEWS	Tue May 28 19:52:14 2019 +0200
     1.3 @@ -28,8 +28,8 @@
     1.4  feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
     1.5  via "isabelle update_cartouches -t" (available since Isabelle2015).
     1.6  
     1.7 -* Infix operators that begin or end with a "*" can now be paranthesized
     1.8 -without additional spaces, eg "(*)" instead of "( * )". Minor
     1.9 +* Infix operators that begin or end with a "*" are now parenthesized
    1.10 +without additional spaces, e.g. "(*)" instead of "( * )". Minor
    1.11  INCOMPATIBILITY.
    1.12  
    1.13  * Mixfix annotations may use cartouches instead of old-style double
    1.14 @@ -252,7 +252,7 @@
    1.15  equation no longer tuples the arguments on the right-hand side.
    1.16  INCOMPATIBILITY.
    1.17  
    1.18 -* Theory HOL-Library.Multiset: the <Union># operator now has the same
    1.19 +* Theory HOL-Library.Multiset: the \<Union># operator now has the same
    1.20  precedence as any other prefix function symbol.
    1.21  
    1.22  * Theory HOL-Library.Cardinal_Notations has been discontinued in favor