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
\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
following a suggestion by Jasmin as far as I remember.
We have the latex macro already since Isabelle/a33ecf47f0a0 (haftmann
2010).
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
