Re: [isabelle] CHAR ''\092''
I remember having run into the same problem a while ago. At that time, I just used the
nibble notation, i.e., Char Nibble5 NibbleC as in
"backsl = ''This string contains a '' @ Char Nibble5 NibbleC # ''backslash''"
This is of course not a solution or explanation, just a workaround.
On 30/06/15 14:56, Lars Noschinski wrote:
I noticed that in HOL terms
''\091'' is the string ''[''
''\093'' is the string '']''
''\092'' is not the backslash, but gives a syntax error.
Why is that and what is the "correct" syntax for a term level string
containing a backslash?
BTW, using the string cartouche syntax in
~~/src/HOL/ex/Cartouche_Examples works here.
This archive was generated by a fusion of
Pipermail (Mailman edition) and