Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Markup in Comment


view this post on Zulip Email Gateway (Aug 18 2022 at 18:30):

From: Jens Doll <jd@cococo.de>
Hello all,

could someone kindly tell me, what the pattern

// some text @{text A} more text

means and how this looks like when printed?

I am currently working on a new version of my software Elbe and would
like to process these patterns.

Jens
http://cococo.de /Elbe

view this post on Zulip Email Gateway (Aug 18 2022 at 18:30):

From: Jens Doll <jd@cococo.de>
Hello all,

the matter of the question is still a miracle to me. Could someone kindly tell me, what the pattern

// ..... @{text A} .............

means and how this looks like when printed?

I am currently working on a new version of my software Elbe and would
like to process these patterns.

Jens
http://cococo.de /Elbe

view this post on Zulip Email Gateway (Aug 18 2022 at 18:31):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jens,

@{text ...} is just a regular document antiquotation, which involves no
formal checks. See further §4.2 of the Isabelle reference manual.

Hope this helps,
Florian
signature.asc


Last updated: Nov 21 2024 at 12:39 UTC