Email Gateway (Aug 04 2023 at 12:42): Email Gateway (Aug 04 2023 at 12:42):From: Diego Machado Dias <diegodias.m@gmail.com>
Dear Makarius,
I've used the unicode character "⋒" (U+22D2) to represent a binary operator
in a theory in Isabelle and would like to know if it would be possible for
this symbol to be included in the default Isabelle font which will shipped
in the next release of Isabelle. My formalisation is not the only one which
would benefit from the inclusion of this symbol in the default Isabelle
fonts: the symbol is already used at least in the following AFP entry:
Concurrent
Refinement Algebra and Rely Quotients
<https://www.isa-afp.org/entries/Concurrent_Ref_Alg.html>.
When extending IsabelleSymbols.sfd locally, I take the missing glyph from
"DejaVu Sans Condensed", and to extend "IsabelleSymbolsBold.sfd", I take
the glyph from "DejaVu Sans". For the latex mapping in
lib/texinputs/isabellesym.sty, I
use \newcommand{\isasymCap}{\isamath{\Cap}}. The name chosen for the symbol
within Isabelle is not important to me, and I would be happy with any other
arbitrary name.
Thanks,
Diego Dias
Last updated: Apr 28 2024 at 20:16 UTC