Re: [isabelle] Antiquotation for theorem names



On Wed, 24 Mar 2010, Christian Sternagel wrote:

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

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






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