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 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;
›
This gives a lexical error, though I guess it should interpret as plain
"a\<^isub>1". (Alas I have no suitable literature at hand which would
give an exact specification of a string's lexical structure in ML).
So, is this the intended behaviour? I have stumbled over that issue
while trying to generate code involvings strings of that kind.
Any suggestions welcome.
Thanks a lot,
Florian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
