--- a/src/Tools/SML/Examples.thy Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Tools/SML/Examples.thy Sat Apr 19 17:23:05 2014 +0200
@@ -23,7 +23,6 @@
SML_file "factorial.sml"
-
text {*
The subsequent example illustrates the use of multiple 'SML_file'
commands to build larger Standard ML projects. The toplevel SML
@@ -34,4 +33,20 @@
SML_file "Example.sig"
SML_file "Example.sml"
+
+text {*
+ 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.
+*}
+
+SML_export {* val f = factorial *} -- {* re-use factorial from SML environment *}
+ML {* f 42 *}
+
+SML_import {* val println = Output.writeln *}
+ -- {* re-use Isabelle/ML channel for SML *}
+
+SML_import {* val par_map = Par_List.map *}
+ -- {* re-use Isabelle/ML parallel list combinator for SML *}
+
end