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

[Lars Noschinski]

On 31.03.2014 16:04, Makarius wrote:
> 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.
I tried to load Pure.ML with SML_File, but this probably qualifies as a
"too exotic" build process ;)

   -- Lars