Email Gateway (Aug 18 2022 at 16:33): 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
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: Nov 21 2024 at 12:39 UTC