[isabelle-dev] Vampire

[Makarius]

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