Email Gateway (Aug 18 2022 at 12:14): Email Gateway (Aug 18 2022 at 12:14):From: Denis Bueno <dbueno@gmail.com>
I'm having a few problems formatting my theory.
Is there a way to make syntax appear for an arbitrary definition
without changing the each use? I thought "notation" would do this,
but my typesetting didn't change.
For example, can I issue a command at the top of my theory that will
change "card A" into "|A|" in LaTeX output, without having to change
every occurrence of "card A" into something else?
Also, can I still do this (e.g. for a binary function constant) even
if there is no associated ASCII infix syntax for it?
Importing LaTeXsugar and OptionalSugar into my theory didn't seem to
change anything. In particular, e.g., "\<not>(\<exists M. ...)" does
not produce the the exists symbol with a slash through it, as the
"sugar for LaTeX documents" pdf [0] says it should; it produces what
"\<not>(\<exists> M. ...)" would produce normally. As another
example, the empty set is still typeset as "{}". (I added a
\usepackage{amssymb} to root.tex as indicated by "sugar...".)
[0] http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf
Email Gateway (Aug 18 2022 at 12:14):From: Makarius <makarius@sketis.net>
The Isabelle document preparation system merely presents your sources.
Only explicit antiquotations like @{term "x + y"} are printed again.
The 'notation' command allows you to write your sources in the way you
expect, but you have to do it yourself. (The document preparation system
manages to produce quite good results without even understanding the
structure of the theory sources.)
Makarius
Email Gateway (Aug 18 2022 at 12:15):From: Makarius <makarius@sketis.net>
The sugar only affects things printed via embedded antiquotations such as
@{thm my_fact}. Regular source text really needs to be written the way it
should be typeset. So yes, you will have to replace {} by \<emptyset> in
the theory source, if you prefer that symbol over the other.
Makarius
Email Gateway (Aug 18 2022 at 12:15):From: Denis Bueno <dbueno@gmail.com>
Ah, okay, thanks for the clarification.
Is there a reason you can think of, or a procedure I might use to
debug, for why importing LaTeXsugar and OptionalSugar appear not to
affect e.g. the printing of the emptyset? Or do I need to edit the
document, e.g. to use \<emptyset> instead of {}?
Email Gateway (Aug 18 2022 at 12:15):From: Tobias Nipkow <nipkow@in.tum.de>
The only symbol for the empty set in Isabelle is "{}". Hence you can
only obtain the latex \emptyset via antiquotations, not in the sources.
However, you can modify Library/LaTeXsugar as follows:
Replace
syntax (latex output)
"_emptyset" :: "'a set" ("...")
translations
"_emptyset" <= "{}"
by
notation (latex)
"{}" ("\<emptyset>")
If you import LaTeXsugar into a theory, you may now use \<emptyset> in it.
We may modify LaTeXsugar for the next release accordingly.
Tobias
Denis Bueno schrieb:
Last updated: May 03 2024 at 04:19 UTC