Re: [isabelle] syntax issue in document preparation



Yes, @{thm [source] name} is the way to do it.

Cheers,
Gerwin

> On 31.12.2014, at 06:17, Christian Sternagel <c.sternagel at gmail.com> wrote:
>
> 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
>>
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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