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

[Makarius]

On Tue, 29 Dec 2015, Makarius wrote:

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

Here is an updated summary according to Isabelle2016-RC0, with further 
notes at the bottom:


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

* Support for more arrow symbols, with rendering in LaTeX and Isabelle
   fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow>
   \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>


*** Prover IDE -- Isabelle/Scala/jEdit ***

* Additional abbreviations for syntactic completion may be specified in
   $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with
   support for simple templates using ASCII 007 (bell) as placeholder.


*** Document preparation ***

* HTML presentation uses the standard IsabelleText font and Unicode
   rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former
   print mode "HTML" loses its special meaning.


*** HOL ***

* Some old and rarely used ASCII replacement syntax has been removed.
   INCOMPATIBILITY, standard syntax with symbols should be used instead.
   The subsequent commands help to reproduce the old forms, e.g. to
   simplify porting old theories:

   notation iff  (infixr "<->" 25)

   notation Times  (infixr "<*>" 80)

   type_notation Map.map  (infixr "~=>" 0)
   notation Map.map_comp  (infixl "o'_m" 55)

   type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)

   notation FuncSet.funcset  (infixr "->" 60)
   notation FuncSet.extensional_funcset  (infixr "->\<^sub>E" 60)

   notation Omega_Words_Fun.conc (infixr "conc" 65)

   notation Preorder.equiv ("op ~~")
     and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)

   notation (in topological_space) tendsto (infixr "--->" 55)
   notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
   notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)

   notation NSA.approx (infixl "@=" 50)
   notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
   notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)

* The alternative notation "\<Colon>" for type and sort constraints has
   been removed: in LaTeX document output it looks the same as "::".
   INCOMPATIBILITY, use plain "::" instead.

* Library/Monad_Syntax: notation uses symbols \<bind> and \<then>.
   INCOMPATIBILITY.



Note that the IsabelleText font provides new glyphs for \<bind> \<then> 
\<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> 
\<longlonglongleftarrow> \<longlonglongrightarrow> by stretching official 
code-point descriptions (literally) very far.

With standard Unicode fonts, these may look bad, or just show up as black 
or white box.  We are privileged to live in a space of infinitely many 
Isabelle symbols.

The following resources might be generally interesting to explore 
possibilities in LaTeX:

   http://mirrors.ctan.org/info/symbols/comprehensive/symbols-a4.pdf
   http://detexify.kirelabs.org
   http://milde.users.sourceforge.net/LUCR/Math


 	Makarius