Re: [isabelle] syntax annotations

Works perfectly fine!


> 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).
> cheers
> chris
> On 11/19/2012 09:21 PM, Diego Marmsoler wrote:
>> 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.