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
this:
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.
```

Makarius

```

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