# [isabelle] backslashes in constant names

Hello,


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)

constdefs
"\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)?

Thanks,

Stephan



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