[isabelle] News: ( * ) -> (*)

[Tobias Nipkow]

Now that the comment syntax (* ... *) within terms has gone:

Infix operators that begin or end with a "*" can/must now be paranthesized
without additional spaces, eg "(*)" instead of "( * )".

Enjoy!
Tobias

[Makarius]

Post by Tobias Nipkow
Infix operators that begin or end with a "*" can/must now be paranthesized
without additional spaces, eg "(*)" instead of "( * )".

This refers to the following Isabelle repository version:
http://isabelle.in.tum.de/repos/isabelle/rev/5f83db57e8c2

Thus it will be part of the next official release, presumably
Isabelle2019 in June 2019. In Isabelle2018 (August 2018) we've had the
first stage of that update of infix syntax, in Isabelle2019 it will be
completed as described here.


Makarius