[isabelle] syntax annotations


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
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?


Best regards,


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