diff -r faddc6504177 -r c15bcd87f47c doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Fri Nov 17 02:19:52 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Fri Nov 17 02:19:54 2006 +0100
@@ -344,8 +344,9 @@
   \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
   \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
   \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
+  \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
   \indexml{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
-  \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
+  \indexml{Isar.goal}\verb|Isar.goal: unit -> thm list * thm| \\
   \end{mldecls}
 
   \begin{description}
@@ -363,6 +364,9 @@
   \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
   (\secref{sec:generic-context}).
 
+  \item \verb|Isar.goal ()| picks the goal configuration from \verb|Isar.state ()|, consisting on the current facts and the goal
+  represented as a theorem according to \secref{sec:tactical-goals}.
+
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%