On 04/07/18 12:18, Lawrence Paulson wrote:
> 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.
This SML'97 stuff is indeed alien to Isabelle/ML, and semantically wrong.
The canonical operations always operate on Isabelle symbols, e.g. see
Symbol.trim_blanks.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
