Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Backtick


view this post on Zulip Email Gateway (Aug 18 2022 at 16:33):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 16:45):

From: Victor Porton <porton@narod.ru>
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?

\--
Victor Porton - http://portonvictor.org


Last updated: Mar 29 2024 at 12:28 UTC