[isabelle] syntax annotations



Hi,

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
2)	Actually it is not even a symbol, but rather it is a makro which
takes an argument and draws an arrow above it.

Does someone have an idea how I could solve this problem?

Thanks.


Best regards,

Diego






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