[isabelle] Antiquotation for theorem names



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.