--- a/doc-src/IsarImplementation/Thy/Integration.thy Wed Oct 28 22:18:00 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Integration.thy Wed Oct 28 22:26:00 2009 +0100
@@ -274,7 +274,8 @@
@{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.goal: "unit -> thm"} \\
+ @{index_ML Isar.goal: "unit ->
+ {context: Proof.context, facts: thm list, goal: thm}"} \\
\end{mldecls}
\begin{description}
@@ -293,8 +294,9 @@
"Isar.state ()"}, analogous to @{ML Context.proof_of}
(\secref{sec:generic-context}).
- \item @{ML "Isar.goal ()"} picks the tactical goal from @{ML
- "Isar.state ()"}, represented as a theorem according to
+ \item @{ML "Isar.goal ()"} produces the full Isar goal state,
+ consisting of proof context, facts that have been indicated for
+ immediate use, and the tactical goal according to
\secref{sec:tactical-goals}.
\end{description}
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Wed Oct 28 22:18:00 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Wed Oct 28 22:26:00 2009 +0100
@@ -335,7 +335,8 @@
\indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
\indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
\indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
- \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit -> thm| \\
+ \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit ->|\isasep\isanewline%
+\verb| {context: Proof.context, facts: thm list, goal: thm}| \\
\end{mldecls}
\begin{description}
@@ -353,7 +354,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 tactical goal from \verb|Isar.state ()|, represented as a theorem according to
+ \item \verb|Isar.goal ()| produces the full Isar goal state,
+ consisting of proof context, facts that have been indicated for
+ immediate use, and the tactical goal according to
\secref{sec:tactical-goals}.
\end{description}%