Re: [isabelle] syntax issue in document preparation



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.