Re: [isabelle] Backtick



Am 18.12.2010 um 18:55 schrieb Victor Porton:

> Formulas may be quotes by backticks, like `X=0`.
>  
> But what if a formula to be quoted contains backtick, like "f`a". Can we quote such a formula?

This is explained on p. 29 of the Isar manual, in the "Lexical Matters" section:

http://isabelle.in.tum.de/doc/isar-ref.pdf

"The syntax of string admits any characters, including newlines; “"” (double-quote) and “\” (backslash) need to be escaped by a backslash; arbitrary character codes may be specified as “\ddd”, with three decimal digits. Alternative strings according to altstring are analogous, using single backquotes instead."

Jasmin






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