Re: [isabelle] Problem with translations
On Tue, 12 Sep 2006, Burkhart Wolff wrote:
> "_SCHEME6 N D P" == (prop)"N == (_AXIOM3 D P)"
> According to the Isar-Reference Manual, this syntax still
> exists, allowing to specify optionally the non-terminal
> for the lhs or rhs of the translation.
> Unfortunately, the syntactic category "prop" is no longer recognized
> by the Isar Parser
Just use quotes around "prop". The name/nameref category happens to allow
non-quoted identifiers as well, but these occur so often that it is easy
to forget the more general form of explicitly quoted names.
This archive was generated by a fusion of
Pipermail (Mailman edition) and