Re: [isabelle] syntax annotations

Dear Diego,

this can be achieved using raw symbols (see section 1.2.1 "Strings of symbols" in the implementation manual [isabelle doc implementation]) as follows. If you want to mark a function "f" (i.e., f is an existing constant in your theory), you can add

notation (latex)
  f ("\<^raw:\overleftarrow{f}>")

where (latex) specifies that this notation should only be used in latex mode (without it you would always see the new syntax, which would not be very readable). Inside a \<^raw:...> you can use arbitrary latex code (for PDF LaTeX document preparation) and you can use several \<^raw:...> symbols to give arguments to macros, e.g.,

notation (latex)
  f ("\<^raw:\fsyntax{>_\<^raw:}>")

would use the macro \fsyntax{x} (which you can freely define in your LaTeX sources) in order to typeset the term "f x". If "f" would be used without argument, the macro would not be used, but you could do

notation (latex)
  f ("\<^raw:\fsyntaxnoarg>") and
  f ("\<^raw:\fsyntax{>_\<^raw:}>")

to also give special syntax for f without argument (note that order is important here, if you would define the no-argument syntax last, it would always be used).



On 11/19/2012 09:21 PM, 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
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.