Re: [isabelle] sml standard library

If you use Poly/ML or SML/NJ, the Standard ML Basis Library is available. Because of the very lengthy gestation of the Basis Library, you'll find many incompatibilities among different versions of these compilers.

However, as you have noticed, Isabelle provides a non-standard top- level that on some respects resembles pre-1997 ML. Isabelle also provides its own libraries, particularly for many things that were omitted from the Basis. See src/Pure/General.


On 7 Nov 2005, at 17:43, Sean McLaughlin wrote:

I've noticed that some of the functions from library.ML do not compile under the usual standard library. Eg, "use "library.ML" crashes with functions like "space_implode" which have the wrong type, changing 'string' for 'char'. What standard
sml library is Isabelle using?

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.