Re: [isabelle] Problem with translations



On Tue, 12 Sep 2006, Burkhart Wolff wrote:

> translations 
>  "_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.


	Makarius





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