# HG changeset patch
# User wenzelm
# Date 1207836953 -7200
# Node ID e99719e70925255fb953b992a5aa54a38d49560f
# Parent  b5fd3ad271ec7a0b441cc9d653effbd7bc903da2
Isar.goal: tactical goal only;

diff -r b5fd3ad271ec -r e99719e70925 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Thu Apr 10 15:04:11 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Thu Apr 10 16:15:53 2008 +0200
@@ -335,7 +335,7 @@
   \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.goal}\verb|Isar.goal: unit -> thm list * thm| \\
+  \indexml{Isar.goal}\verb|Isar.goal: unit -> thm| \\
   \end{mldecls}
 
   \begin{description}
@@ -353,8 +353,8 @@
   \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}.
+  \item \verb|Isar.goal ()| picks the tactical goal from \verb|Isar.state ()|, represented as a theorem according to
+  \secref{sec:tactical-goals}.
 
   \end{description}%
 \end{isamarkuptext}%
diff -r b5fd3ad271ec -r e99719e70925 doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Thu Apr 10 15:04:11 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Thu Apr 10 16:15:53 2008 +0200
@@ -275,7 +275,7 @@
   @{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 list * thm"} \\
+  @{index_ML Isar.goal: "unit -> thm"} \\
   \end{mldecls}
 
   \begin{description}
@@ -294,9 +294,9 @@
   "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}.
+  \item @{ML "Isar.goal ()"} picks the tactical goal from @{ML
+  "Isar.state ()"}, represented as a theorem according to
+  \secref{sec:tactical-goals}.
 
   \end{description}
 *}