On Mon, 26 Jan 2015, Florian Haftmann wrote:
I think it is best if I find a possibility to print strings in a way
that is both digestible for Isabelle/ML and (S)ML.
If it is just for generated sources, you could use "\092" for backslash
and thus escape further special treatment as Isabelle sy
> I think the following thread is related to your question:
>
> http://comments.gmane.org/gmane.science.mathematics.logic.isabelle.user/10007
I see. I think it is best if I find a possibility to print strings in a
way that is both digestible for Isabelle/ML and (S)ML.
Florian
>
>
> O
I think the following thread is related to your question:
http://comments.gmane.org/gmane.science.mathematics.logic.isabelle.user/10007
On 01/26/2015 09:30 AM, Florian Haftmann wrote:
I have some doubt whether the parsing of strings by Isabelle/ML conforms
to plain ML.
See the following exampl
I have some doubt whether the parsing of strings by Isabelle/ML conforms
to plain ML.
See the following examples.
ML_val ‹
val s = "a\nb";
writeln s;
›
OK, seems quite plausible.
ML_val ‹
val s = "a\\b";
writeln s;
›
OK, seems quite plausible.
ML_val ‹
val s = "a\\<^isub>1";
writeln s;
›
Thi
