Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] document antiquotation for locale names

view this post on Zulip Email Gateway (Aug 19 2022 at 09:44):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,

I found the document antiquotation @{class c} for printing a class name
(I guess). Is there a similar antiquotation for names of locales? If
not, how about adding one, just for completeness?

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 10:03):

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

I found the document antiquotation @{class c} for printing a class name
(I guess). Is there a similar antiquotation for names of locales?

I don't think so.

If not, how about adding one, just for completeness?

I would recommend to implement it first privately, a way which to some
extent even follows the Isabelle documentation itself (cf.
Doc/antiquote_setup.ML, which is a nice tutorial also). There are a
couple of questions (e.g. what to refer to exactly? locale names? locae
expressions?) which should be ironed out before such a thing becomes
official and thus making it harder to reshape it.

Cheers,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC