--- a/doc-src/IsarImplementation/Thy/ML.thy Tue Oct 19 19:16:27 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Tue Oct 19 19:20:02 2010 +0100
@@ -674,6 +674,7 @@
text %mlref {*
\begin{mldecls}
+ @{index_ML_type "'a Unsynchronized.ref"} \\
@{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
@{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\
@{index_ML "op :=": "'a Unsynchronized.ref * 'a -> unit"} \\
@@ -691,10 +692,10 @@
mutability. Existing operations @{ML "!"} and @{ML "op :="} are
unchanged, but should be used with special precautions, say in a
strictly local situation that is guaranteed to be restricted to
- sequential evaluation -- now and in the future. *}
+ sequential evaluation --- now and in the future. *}
-section {* Thread-safe programming *}
+section {* Thread-safe programming \label{sec:multi-threading} *}
text {* Multi-threaded execution has become an everyday reality in
Isabelle since Poly/ML 5.2.1 and Isabelle2008. Isabelle/ML provides