[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 HOL)

  "\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 MHonArc.