--- 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%