[isabelle] CHAR ''\092''

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.