Re: [isabelle] CHAR ''\092''

Dear Lars,

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

definition backsl
where [simplified]:
  "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:
Hi everyone,

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.

   -- Lars

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