Dear friends of Poly/ML, or Standard ML in general,
Isabelle2013-2 is now available from the usual mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/
It is mainly an environment for interactive and automated theorem proving, but the integration of Isabelle/ML into the Prover IDE makes it suitable for general Standard ML development (potentially in teaching scenarios).
After downloading / unpacking / running the main application of Isabelle/jEdit, the Documentation panel on the right-hand side gives quick access to Examples, notably src/HOL/ex/ML.thy for some Isabelle/ML basics.
The manual on Isabelle/jEdit in the same panel provides further details on the IDE, which is based on the jEdit text editor.
Makarius