Re: [isabelle] syntax issue in document preparation

Dear Gergely,

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).

The reason why @{term path_induct} works (even though, no constant of this name exists), is that it fits the "ident" token category (see isar-ref, ~ page 51) and is just interpreted as some variable, while "path.induct" is of category "longident" (which is not allowed for variables, I think) and thus interpreted as constant name.

This difference is also visible in Isabelle/jEdit, where in

  @{term path_induct}

"path_induct" is blue (and identified as "free variable" by C-hover) and in

  @{term path.induct}

"path.induct" is black (and identified as belonging to the term language by C-hover).



On 12/30/2014 05:35 PM, Gergely Buday wrote:

in Nominal/Ex/Lambda.thy a proof command refers to path.induct . Now I
cannot use

    @{term path.induct}

in a proof document as it fails, but

    @{term path_induct}

which works but I wonder as it does not exist as a valid term.

Do I not understand something important about terms and antiquotations?

- Gergely

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