Re: [isabelle] arities syntax in Isar-style theory files



On Wednesday 13 September 2006 18:36, Jeremy Dawson wrote:
> The reference manual gives the following example
>
> arities
>    foo :: ({logic}) logic
>    foo :: ({}) term

Try using quotes around the braces, like this:

arities
   foo :: ("{logic}") logic
   foo :: ("{}") term

The parser for sorts (defined in Pure/Isar/outer_syntax.ML) can accept an 
alphanumeric name, or a quoted string, but not anything starting with a 
curly-brace character. I think the confusion in the reference manual might 
arise because quote marks are omitted when Isabelle syntax is typeset.

Hope this helps.

- Brian Huffman





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