*To*: "'Christian Sternagel'" <c-sterna at jaist.ac.jp>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] syntax annotations*From*: "Diego Marmsoler" <marmsoler_diego at yahoo.it>*Date*: Mon, 26 Nov 2012 15:51:14 +0100*In-reply-to*: <50AB4D31.90904@jaist.ac.jp>*References*: <000901cdc693$6ebb4030$4c31c090$@yahoo.it> <50AB4D31.90904@jaist.ac.jp>*Thread-index*: AQLQBwluZnRhQJJC68t4JC7IdPGYtQJ5LTWtlePzcpA=

Works perfectly fine! Thanks. Diego > 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

**References**:**[isabelle] syntax annotations***From:*Diego Marmsoler

**Re: [isabelle] syntax annotations***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Length of Proofs
- Next by Date: Re: [isabelle] [symmetric]-attribute changes variable names
- Previous by Thread: Re: [isabelle] syntax annotations
- Next by Thread: Re: [isabelle] syntax annotations
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list