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

Makarius makarius at sketis.net
Tue Dec 29 18:17:06 CET 2015

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


More information about the isabelle-dev mailing list