[isabelle-dev] NEWS: command-line terminator "; " is no longer accepted

[Makarius]

*** System ***

* Historical command-line terminator ";" is no longer accepted.  Minor
INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete
semicolons from theory sources.


This refers to Isabelle/5ff61774df11.

The command-line terminator was an artifact of the TTY loop and has 
encumbered us long enough.  Now the popular keyword ";" has become free as 
literal token in the outer syntax.

It is presently unused, but the Eisbach proof method language could use it 
as notation for THEN_ALL_NEW, for example.


 	Makarius

----------------------------------------------------------------------------
                   http://stop-ttip.org  774,957 people so far
----------------------------------------------------------------------------