[isabelle-dev] Vampire

[Lawrence Paulson]

Well, there’s this:

> String.translate (fn c => if Char.isSpace c then "" else str c) " y   e   s  ";
val it = "yes": string

No idea what Isabelle/ML does to these primitives however.

Larry

> On 4 Jul 2018, at 11:11, Blanchette, J.C. <j.c.blanchette at vu.nl> wrote:
> 
> I just copied old code I inherited from Sascha Böhm and his Vampire noncommercial. For sure there are endlessly many ways in which we could make Isabelle and Sledgehammer more user friendly. In Qt/C++, we had a "stripWhiteSpace" function that would do the trick. But string manipulation in ML is like pulling teeth. If you happen to know which function I can call, I'll gladly change the code.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180704/290a7834/attachment-0002.html>