*** ML ***
* Original PolyML.pointerEq is retained as a convenience for tools that
don't use Isabelle/ML (where this is called "pointer_eq").
* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
option ML_environment to select a named environment, such as "Isabelle"
for Isabelle/ML, or "SML" for official Standard ML. It is also possible
to move toplevel bindings between environments, using a notation with
">" as separator. For example:
declare [[ML_environment = "Isabelle>SML"]]
ML ‹val println = writeln›
declare [[ML_environment = "SML"]]
ML ‹println "test"›
declare [[ML_environment = "Isabelle"]]
ML ‹println› ― ‹not present›
The Isabelle/ML function ML_Env.setup defines new ML environments. This
is useful to incorporate big SML projects in an isolated name space, and
potentially with variations on ML syntax (existing ML_Env.SML_operations
observes the official standard).
This refers to Isabelle/7414ce0256e1.
It is the current state of various ongoing discussions about
incorporating other ML applications into the Isabelle environment (e.g.
OpenTheory, Metis, MetiTarski HOL4, ProofPower). There are two
motivations for this:
(1) Developing these tools in the Isabelle Prover IDE
(instead of vi or Emacs)
(2) Using these tools inside Isabelle
A bit more work is required to make this really work in practice, but
this is an important stepping stone towards routine use of "ML
virtualization" (Isabelle can load Isabelle/Pure into itself, so it
should be able to load less complex applications, too).
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
