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.


> On 4 Jul 2018, at 11:11, Blanchette, J.C. <j.c.blanche...@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.

isabelle-dev mailing list

Reply via email to