Re: [isabelle] syntax issue in document preparation



I think @{thm [source] some_theorem_name} might work (i.e., print the name instead of the theorem statement; but it has been a while since I used this and I haven't had time to check).

cheers

chris

On 12/30/2014 07:59 PM, Gergely Buday wrote:
Christian Sternagel wrote:

maybe you wanted to type

   @{thm path.induct}

which would work, since "path.induct" is the name of a theorem (from the
nominal2 repository, which I'm just guessing you are referring to).

Sorry I did not include a rationale for this. My aim is a list that
contains theorem names and the theorems itself. First I used plain
text but the underscores in theorem names break latex typesetting as
it thinks as if it were some subscript and missing the math mode $.
Replacing underscores with backslash-underscore is tedious by hand. So
I tried the following scheme:

     \item @{term alpha_lst} @{thm alpha_lst}

Should I use another antiquotation keyword for such theorem names as
path.induct? It would be nice if Isabelle checked its validity.

- Gergely





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