[isabelle-dev] NEWS: Isabelle support for Standard ML

[Makarius]

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.
>
>
> This refers to Isabelle/20cf88cd3188.  It is one of the things that have been 
> in principle possible all the time, but required a bit longer to get through 
> the pipeline from the Ural.

I need to advertize this more emphatically, since the full consequences of 
it may not be immediately clear.

What we have here is the Isabelle Prover IDE technology used for something 
that is not Isabelle, namely official Standard ML.  It is just a 
coincidence that it runs within the same Poly/ML runtime system -- there 
is no direct connection to the Isabelle/ML world.

This means regular SML projects can be edited with it, assuming that the 
"build" process is not too exotic --- just the typical list of "use" 
statements (without nesting) that need to be replaced by 'SML_file' here.

Another canonical application is for teaching SML.


If we would have had that 10-20 years ago, Standard ML would be a bit more 
popular today.


 	Makarius