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.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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
