Isabelle2016 has removed quite a lot of old ASCII syntax, and made
Isabelle symbols the default where old ASCII syntax is still available.
A notable exception is lifting_syntax with its old-style ASCII-only
notation, see
http://isabelle.in.tum.de/repos/isabelle/annotate/aeee0a4be6cf/src/HOL/Transfer.thy#l19
locale lifting_syntax
begin
notation rel_fun (infixr "===>" 55)
notation map_fun (infixr "--->" 55)
end
I can imagine two reforms:
* Use proper symbols for these operators (without keeping ASCII
replacement syntax).
* Make the notation a global default, i.e. remove the locale and its
interpretations in applications.
The usual question is which symbols are best.
===> appears to be more frequently used than --->. Based on that
observation, the new triple-line arrow ⇛ could be used for ===>, and
maybe a bold → for --->.
This is only a first idea. There are many possibilities. It is also
possible to add new glyphs to the Isabelle fonts, as long as there are
canonical LaTeX macros for that and some code points in the Unicode charts
that many be (ab)used for our application.
Recent examples of Unicode ab-use in Isabelle symbol interpretation are:
⤏
⇢
⤜
⪢
These need to be viewed in Isabelle/jEdit to see the point: the official
shape of the glyph serves as crude approximation for the intended meaning
in Isabelle.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
