src/Tools/SML/Examples.thy

   evaluates it for some arguments.
 *}
 
 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
   environment is enriched cumulatively within the theory context of
   Isabelle --- independently of the Isabelle/ML environment.
 *}
 
 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