Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Antiquotation for theorem names

Email Gateway (Aug 18 2022 at 14:57):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
In isar-ref, I found the antiquiation @{theory A}, where 'A' is
guaranteed to refer to a valid ancestor theory. Is the same available
for theorem names, that is, something like:

@{lemmas l1 ... lN} where 'l1' to 'lN' are guaranteed to be the names of
existing lemmas and the result after document preparation is for example

\isa{l1}, ..., and \isa{lN}

(I know, there is not real a consensus on whether there should be a
comma in front of 'and' or not... but that is a different story :))?

If this is not available, would it be a reasonable feature to have? What
do you think?

cheers

chris

Email Gateway (Aug 18 2022 at 14:58):

From: Makarius <makarius@sketis.net>
By using something like @{thm [source] NAME} you get the check and a
literal NAME in the text. You can surround it by 'and' commas or
whatever.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC