Email Gateway (Aug 18 2022 at 14:57): 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: Apr 19 2024 at 20:15 UTC