Re: [isabelle] Special character references in LaTeX

On Wed, 27 Aug 2014, W. Douglas Maurer wrote:

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?

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.