[isabelle-dev] NEWS: print mode ASCII vs. xsymbols

[Makarius]

*** General ***

* Former "xsymbols" syntax with Isabelle symbols is used by default,
without any special print mode. Important ASCII replacement syntax
remains available under print mode "ASCII", but less important syntax
has been removed (see below).



*** HOL ***

* Some old and rarely used ASCII replacement syntax has been removed.
INCOMPATIBILITY, standard syntax with symbols should be used instead.


*** System ***

* Command-line tool "isabelle console" enables print mode "ASCII".


This refers to Isabelle/0a5dd617a88c.  A bit more changes may follow 
later.


 	Makarius