--- a/src/Doc/IsarImplementation/Integration.thy Tue Apr 09 15:29:25 2013 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy Tue Apr 09 15:37:23 2013 +0200
@@ -85,9 +85,10 @@
\item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
state if available, otherwise raises @{ML Toplevel.UNDEF}.
- \item @{ML "Toplevel.debug := true"} makes the toplevel print further
- details about internal error conditions, exceptions being raised
- etc.
+ \item @{ML "Toplevel.debug := true"} enables low-level exception
+ trace of the ML runtime system. Note that the result might appear
+ on some raw output window only, outside the formal context of the
+ source text.
\item @{ML "Toplevel.timing := true"} makes the toplevel print timing
information for each Isar command being executed.