Email Gateway (Aug 19 2022 at 15:38): Email Gateway (Aug 19 2022 at 15:38):From: Holden Lee <hl422@cam.ac.uk>
I'd like to put in some comments like so:
proof -
...
-- "some typeset math here like $a \in A$"
...
but it seems like \ can't be used, and \\ doesn't escape it. What's the
correct way?
-Holden
Email Gateway (Aug 19 2022 at 15:38):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Holden,
if you use the delimiters {* and *} instead of " " for the LaTeX text, then antiquotations
and escaping work as expected. In Isabelle2014, you can alternatively use the cartouche
\<open> and \<close>. Instead of an inline comment introduced by --, you can also use
regular text blocks with txt as in
proof
...
txt {* $a \in A$ *}
..
end
Best,
Andreas
Email Gateway (Aug 19 2022 at 15:38):From: Makarius <makarius@sketis.net>
Yes. Moreover, there is usually little need to produce actual LaTeX math
in Isabelle documents. You can just use interpreted or uninterpreted
antiquotations like this:
txt {* @{prop "a \<in> A"} *}
txt {* @{text "a \<in> A"} *}
This has the advantage that the input and typeset output is uniform
according to Isabelle standards, although the pseudo-math mode of
isabelle.sty is a bit weaker than actual math mode.
Makarius
Email Gateway (Aug 19 2022 at 15:39):From: "W. Douglas Maurer" <maurer@gwu.edu>
I have also had problems with comments starting with -- which is why
I always use comments contained in (* and *) (this has always worked
for me, including backslashes).
Email Gateway (Aug 19 2022 at 16:03):From: Makarius <makarius@sketis.net>
There is a common misunderstanding of "formal comments" within the Isar
language versus "source comments" (* *) that suppress certain parts of the
input for the document preparation system. The latter corresponds to % in
latex, i.e. you use it mainly to "comment-out" material that is not part
of the proper document.
So the problem of (* *) within actual Isabelle documents is not just a
conceptual mismatch, but also odd extra white space in unexpected
situations, instead of informative text.
As a rule of thumb, a proper Isabelle document contains little (* *), but
interjects the formally-checked and pretty-printed Isar source with
commands for semi-formal pieces as follows:
section ‹Foo›
subsection ‹Bar›
text ‹Blah blah blub.›
lemma "a = a" .. -- ‹Foo bar blah.›
The "isar-ref" and "system" manuals tell more about Isabelle document
preparation.
Makarius
Email Gateway (Aug 19 2022 at 16:06):From: Makarius <makarius@sketis.net>
That was the thread "How to use latex commands inside proof?" from August
2014. It was answered exhaustively by Andreas Lochbihler and myself, e.g.
see here
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00257.html
Makarius
Email Gateway (Aug 19 2022 at 16:06):From: Makarius <makarius@sketis.net>
This is because the argument to the formal comment "--" needs to be an
atomic item in Isar token syntax. As already shown in earlier examples it
can be done
-- {* like this *}
or
-- ‹like this›
which uses the new cartouche syntax of Isabelle2014.
In general, you have two possibilities:
(1) read the isar-ref manual carefully what the syntax really is
(2) read existing examples and applications carefully how things are
usually done.
If you just make a meta-comment to yourself, without any formal
significance, the (* *) form might be actually what you want, but that is
relatively rare.
Makarius
Last updated: Apr 26 2024 at 12:28 UTC