[isabelle-dev] NEWS: Isabelle support for Standard ML
makarius at sketis.net
Tue Apr 22 16:51:12 CEST 2014
On Tue, 25 Mar 2014, Makarius wrote:
> * Command 'SML_file' reads and evaluates the given Standard ML file.
> Toplevel bindings are stored within the theory context; the initial
> environment is restricted to the Standard ML implementation of
> Poly/ML, without the add-ons of Isabelle/ML. See also
> ~/src/Tools/SML/Examples.thy for some basic examples.
Just a minor update in Isabelle/874bdedb2313:
* Support for official Standard ML within the Isabelle context.
Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import'
and 'SML_export' allow to exchange toplevel bindings between the two
separate environments. See also ~~/src/Tools/SML/Examples.thy for
The updated examples cover SML_import and SML_export as well. The latter
might be useful in loading big chunks of official Standard ML, without
going through the pain to make it conform to Isabelle/ML. A few result
structures or functions for Isabelle/ML can be harvested from the SML
environment in the end.
Nonetheless, such SML applications (especially SML/NJ ones) need to
conform semantically to the Isabelle runtime environment: global refs or
Gansner-Reppy style catch-all exception handlers won't work without the
special assumption of sequentialism and non-interruption.
More information about the isabelle-dev