Email Gateway (Aug 19 2022 at 15:37): Email Gateway (Aug 19 2022 at 15:37):From: "W. Douglas Maurer" <maurer@gwu.edu>
I am using LaTeX to write handouts about Isabelle/Isar for my
students. This allows me to make reference, in the handouts, to
nearly all of the special characters in the Symbols window in jEdit.
Most of them have references in LaTeX which resemble those in the
Symbols window, although some do not; for example, in LaTeX, I have
to write cap instead of Inter, llbracket instead of lbrakk, and so
on. My immediate problem is that there are a very few special
characters whose LaTeX names I have not been able to find, even in my
second edition of the LaTeX Companion. These include \<^bsub>,
\<^esub>, \<^bsup>, \<^esup>, \<lbrace>, \<rbrace>, \<Midarrow>,
\<midarrow>, and \<Tturnstile>. I don't want to have to draw these in
by hand on my handouts. Is there any way I can get any of these to
come out of LaTeX? Thanks! -Douglas
Email Gateway (Aug 19 2022 at 15:37):From: Makarius <makarius@sketis.net>
Instead of raw LaTeX you can use the Isabelle document preparation system
with its predefined mapping from Isabelle symbols to LaTeX macros. See
the "isar-ref" manual chapter 4, or the "system" manual section 3.2 for
quick-start examples.
The Isabelle document antiquotation @{text "\<symbol>"} allows to typeset
the given symbol (or more) the way it is normally done, but without any
formal meaning of the text. You don't have to use LaTeX macros directly.
If you just want to see how Isabelle symbols are rendered in LaTeX, see
$ISABELLE_HOME/lib/textinputs/isabellesym.sty -- it corresponds to
"isar-ref" appendix B.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC