src/Tools/SML/Examples.thy
changeset 56618 874bdedb2313
parent 56276 9e2d5e3debd3
child 58616 4257a7f2bf39
     1.1 --- a/src/Tools/SML/Examples.thy	Thu Apr 17 14:52:23 2014 +0200
     1.2 +++ b/src/Tools/SML/Examples.thy	Sat Apr 19 17:23:05 2014 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4  
     1.5  SML_file "factorial.sml"
     1.6  
     1.7 -
     1.8  text {*
     1.9    The subsequent example illustrates the use of multiple 'SML_file'
    1.10    commands to build larger Standard ML projects.  The toplevel SML
    1.11 @@ -34,4 +33,20 @@
    1.12  SML_file "Example.sig"
    1.13  SML_file "Example.sml"
    1.14  
    1.15 +
    1.16 +text {*
    1.17 +  Isabelle/ML and SML share a common run-time system, but the static
    1.18 +  environments are separate.  It is possible to exchange toplevel bindings
    1.19 +  via separate commands like this.
    1.20 +*}
    1.21 +
    1.22 +SML_export {* val f = factorial *}  -- {* re-use factorial from SML environment *}
    1.23 +ML {* f 42 *}
    1.24 +
    1.25 +SML_import {* val println = Output.writeln *}
    1.26 +  -- {* re-use Isabelle/ML channel for SML *}
    1.27 +
    1.28 +SML_import {* val par_map = Par_List.map *}
    1.29 +  -- {* re-use Isabelle/ML parallel list combinator for SML *}
    1.30 +
    1.31  end