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
~/sr
l
Subject: Re: [isabelle-dev] NEWS: Isabelle support for Standard ML
If you wanted to advertise it on functional programming mailing lists, I
think it would be helpful to eliminate the need for a theory file. I’m not
sure what alternative could be used; I never understood the SML/NJ
Compilation Man
On Mon, 31 Mar 2014, Lars Noschinski wrote:
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 i
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/M
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
~/sr
* 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
