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

On Tue, 30 Jun 2015, Lars Noschinski wrote:

BTW, using the string cartouche syntax in
~~/src/HOL/ex/Cartouche_Examples works here.

That is a slightly different question. In these examples, I've made some experiments about potential futures of Isabelle/HOL syntax.

E.g. one could allow outer cartouches routinely to embed inner syntax items. And within the inner syntax, double quotes for string literals. That would make Isabelle/HOL material look more conventional, although backslashes still have a role as escape.

Here is an example:

  term_cartouche â"a\\b"â

In these experiments I was optimistic and just allowed the backslash in that form. More care would be needed to think about printing that in different contexts.


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