[isabelle-dev] lifting syntax with proper symbols

[Ondřej Kunčar]

As Andreas already mentioned, we've been consistently using the symbol 
\Mapsto for ===> in our papers. Concerning --->, we used \mapsto.

Ondrej

On 03/04/2016 12:36 PM, Andreas Lochbihler wrote:
> Hi Makarius,
>
> How about LaTeX \Mapsto for ===>? This is what I use in my papers
> following Ondrej and Brian's paper on lifting.
>
> I'd be happy to have syntax for ===> enabled by default, as it makes
> transfer and parametricity rules much easier to read. I have no opinion
> on --->.
>
> Andreas
>
> On 04/03/16 11:56, Makarius wrote:
>> 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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev