some SML examples;

--- a/NEWS	Tue Mar 25 13:18:10 2014 +0100
+++ b/NEWS	Tue Mar 25 14:52:35 2014 +0100
@@ -41,7 +41,8 @@
 * Command 'SML_file' reads and evaluates the given Standard ML file.
 Toplevel bindings are stored within the theory context; the initial
 environment is restricted to the Standard ML implementation of
-Poly/ML, without the add-ons of Isabelle/ML.
+Poly/ML, without the add-ons of Isabelle/ML.  See also
+~~/src/Tools/SML/Examples.thy for some basic examples.
 
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***

--- a/src/Pure/Tools/doc.scala	Tue Mar 25 13:18:10 2014 +0100
+++ b/src/Pure/Tools/doc.scala	Tue Mar 25 14:52:35 2014 +0100
@@ -61,7 +61,8 @@
         "src/HOL/ex/Seq.thy",
         "src/HOL/ex/ML.thy",
         "src/HOL/Unix/Unix.thy",
-        "src/HOL/Isar_Examples/Drinker.thy")
+        "src/HOL/Isar_Examples/Drinker.thy",
+        "src/Tools/SML/Examples.thy")
     Section("Examples") :: names.map(name => text_file(name).get)
   }
 

--- a/src/Tools/ROOT	Tue Mar 25 13:18:10 2014 +0100
+++ b/src/Tools/ROOT	Tue Mar 25 14:52:35 2014 +0100
@@ -7,3 +7,8 @@
   theories [condition = ISABELLE_POLYML]
     Examples
 
+session SML in SML = Pure +
+  options [condition = ISABELLE_POLYML]
+  theories
+    Examples
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/SML/Example.sig	Tue Mar 25 14:52:35 2014 +0100
@@ -0,0 +1,6 @@
+signature Example =
+sig
+  type t
+  val a: t
+  val b: t -> t
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/SML/Example.sml	Tue Mar 25 14:52:35 2014 +0100
@@ -0,0 +1,9 @@
+structure Example :> Example =
+struct
+
+type t = int
+
+val a = 0
+fun b x = x + 1
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/SML/Examples.thy	Tue Mar 25 14:52:35 2014 +0100
@@ -0,0 +1,37 @@
+(*  Title:      Tools/SML/Examples.thy
+    Author:     Makarius
+*)
+
+header {* Standard ML within the Isabelle environment *}
+
+theory Examples
+imports Pure
+begin
+
+text {*
+  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 'SML_file' 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 function and
+  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"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/SML/factorial.sml	Tue Mar 25 14:52:35 2014 +0100
@@ -0,0 +1,6 @@
+fun factorial 0 = 1
+  | factorial n = n * factorial (n - 1);
+
+factorial 10;
+factorial 100;
+factorial 1000;