*** 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
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
