--- 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} *}