[isabelle] backslashes in constant names
I recently tried to define constant names that contain backslashes and
ran into a curious behavior of the parser. When I try, say, to declare
"\in" :: "['a, 'a set] => bool" (infixl 50)
"a \in S == a:S"
Isabelle complains about a bad escape character. However, it will
swallow the definition if I write "\\in" (and the output will show
"\in"). Now, when I try to do something similar in Pure, the output will
be "\\in", and the PDF document shows the constant name as ``in.
Should I consider backslashes to be disallowed (as a strict reading of
section 7.2.2 of the reference manual seems to indicate)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and