--- a/doc-src/IsarImplementation/Thy/integration.thy Fri Nov 17 02:19:51 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy Fri Nov 17 02:19:52 2006 +0100
@@ -284,8 +284,9 @@
@{index_ML Isar.main: "unit -> unit"} \\
@{index_ML Isar.loop: "unit -> unit"} \\
@{index_ML Isar.state: "unit -> Toplevel.state"} \\
+ @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
@{index_ML Isar.context: "unit -> Proof.context"} \\
- @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
+ @{index_ML Isar.goal: "unit -> thm list * thm"} \\
\end{mldecls}
\begin{description}
@@ -304,6 +305,10 @@
"Isar.state ()"}, analogous to @{ML Context.proof_of}
(\secref{sec:generic-context}).
+ \item @{ML "Isar.goal ()"} picks the goal configuration from @{ML
+ "Isar.state ()"}, consisting on the current facts and the goal
+ represented as a theorem according to \secref{sec:tactical-goals}.
+
\end{description}
*}