diff -r 40aee0b95ddf -r ab0afd03a042 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Fri Oct 22 16:57:55 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Fri Oct 22 19:03:31 2010 +0100
@@ -100,6 +100,22 @@
   \end{description}
 *}
 
+text %mlantiq {*
+  \begin{matharray}{rcl}
+  @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\
+  \end{matharray}
+
+  \begin{description}
+
+  \item @{text "@{Isar.state}"} refers to Isar toplevel state at that
+  point --- as abstract value.
+
+  This only works for diagnostic ML commands, such as @{command
+  ML_val} or @{command ML_command}.
+
+  \end{description}
+*}
+
 
 subsection {* Toplevel transitions \label{sec:toplevel-transition} *}