makarius at sketis.net
Thu Sep 12 21:16:07 CEST 2013
On Wed, 11 Sep 2013, Florian Haftmann wrote:
>> Do monadic people have a standard Unicode point to render that operator?
>> If yes, we could assign that to \<bind> and use it from STIX (or provide
>> a glyph in the IsabelleText font).
> For LaTeX I once have been using
> following a suggestion by Jasmin as far as I remember.
We have the latex macro already since Isabelle/a33ecf47f0a0 (haftmann
If we find some Unicode point for it, we could reduce the variance of
notation to 2 or even 1. Allocating Unicode slots is a sport of many
subcultures, e.g. people writing text in Klingon (they did not make it
into the official charts, yet).
Looking around in Deja Vu or STIX for a few minutes, I did not find
anything like \<bind> yet, but it might be still there hidden within
thousands of symbols.
More information about the isabelle-dev