[isabelle-dev] Vampire

Makarius makarius at sketis.net
Wed Jul 4 13:23:29 CEST 2018

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


More information about the isabelle-dev mailing list