Email Gateway (Aug 19 2022 at 09:07): Email Gateway (Aug 19 2022 at 09:07):From: Diego Marmsoler <marmsoler_diego@yahoo.it>
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
Email Gateway (Aug 19 2022 at 09:07):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 19 2022 at 09:07):From: Makarius <makarius@sketis.net>
On Mon, 19 Nov 2012, 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
this:
1) \overleftarrow is not part of the Predefined Isabelle symbols
These are merely common defaults. You can always define your own symbols
in LaTeX. The document preparation systems generates sources like this:
\<foo> becomes {\isasymfoo}
\<^foo> becomes \isactrlfoo
2) Actually it is not even a symbol, but rather it is a makro which
takes an argument and draws an arrow above it.
The second form above allows one argument following, normally the image of
another symbol, not arbitrary long text. See e.g. how \<^bold>\<alpha> is
translated.
Beyond that, you can inline auxliary symbols, and use perl (not sed) to
replace their image by something else in latex.
Makarius
Email Gateway (Aug 19 2022 at 09:14):From: Diego Marmsoler <marmsoler_diego@yahoo.it>
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
Last updated: Apr 25 2024 at 08:20 UTC