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

Makarius makarius at sketis.net
Sun Nov 2 20:16:40 CET 2014

*** 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.


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

More information about the isabelle-dev mailing list