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:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and