[isabelle-dev] string and altstring

Christian Sternagel c.sternagel at gmail.com
Thu Aug 15 06:02:46 CEST 2013

Dear all,

currently it is possible to write something like "\"" , "\\", `\``, or 
`\\` (i.e., there are escape sequences for the delimiters of strings and 
altstrings, as well as for backslash).

What many people might be used to from programming languages does not 
work however, e.g., "\n", "\t", ...

For that reason we currently have some abbreviations like the following 
in IsaFoR:

   abbreviation tab :: "char" where
     "tab ≡ Char Nibble0 Nibble9"
   abbreviation newline :: char where
     "newline ≡ Char Nibble0 NibbleA"
   abbreviation carriage_return :: "char" where
     "carriage_return ≡ Char Nibble0 NibbleD"
   abbreviation wspace :: "char list" where
     "wspace ≡ CHR '' '' # newline # tab # carriage_return # []"

(Maybe there is a better solution?)

Would it make sense to allow the most common escape sequences (like 
"\n", "\t", "\r", etc.)? Then I could use

   CHR ''\t'', CHR ''\n'', CHR ''\r'', '' \n\t\r''

instead of the above.

Btw: Why does "CHR ''\013''" result in "Char Nibble0 NibbleA"? Shouldn't 
that be "Char Nibble0 NibbleD"?



More information about the isabelle-dev mailing list