[isabelle-dev] lifting syntax with proper symbols

[Makarius]

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