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