section \<open>Standard ML within the Isabelle environment\<close>
theory Examples imports Pure begin
text\<open>
Isabelle/ML is a somewhat augmented version of Standard ML, with various
add-ons that are indispensable for Isabelle development, but may cause
conflicts with independent projects in plain Standard ML.
The Isabelle/Isar command \<^theory_text>\<open>SML_file\<close> supports official Standard ML within
the Isabelle environment, with full support in the Prover IDE
(Isabelle/jEdit).
Here is a very basic example that defines the factorial functionand
evaluates it for some arguments. \<close>
SML_file \<open>factorial.sml\<close>
text\<open>
The subsequent example illustrates the use of multiple \<^theory_text>\<open>SML_file\<close> commands to build larger Standard ML projects. The toplevel SML environment is
enriched cumulatively within the theorycontext of Isabelle ---
independently of the Isabelle/ML environment. \<close>
text\<open>
Isabelle/ML and SML share a common run-time system, but the static
environments are separate. It is possible to exchange toplevel bindings via
separate commands like this. \<close>
SML_export \<open>val f = factorial\<close> \<comment> \<open>re-use factorial from SML environment\<close>
ML \<open>f 42\<close>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
