doc-src/IsarImplementation/Thy/integration.thy

 
   \begin{mldecls}
   @{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}
 
   \item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},

   after having dropped out of the Isar toplevel loop.
 
   \item @{ML "Isar.context ()"} produces the proof context from @{ML
   "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}
 *}