Re: [isabelle] syntax annotations

On Mon, 19 Nov 2012, Diego Marmsoler wrote:

I have the following problem. I want to use the latex-symbol
"\overleftarrow" to mark a function. However, there are two problems with
1)	\overleftarrow is not part of the Predefined Isabelle symbols

These are merely common defaults. You can always define your own symbols in LaTeX. The document preparation systems generates sources like this:

  \<foo> becomes {\isasymfoo}
  \<^foo> becomes \isactrlfoo

2)	Actually it is not even a symbol, but rather it is a makro which
takes an argument and draws an arrow above it.

The second form above allows one argument following, normally the image of another symbol, not arbitrary long text. See e.g. how \<^bold>\<alpha> is translated.

Beyond that, you can inline auxliary symbols, and use perl (not sed) to replace their image by something else in latex.


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