--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Thu Jun 03 22:17:36 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Thu Jun 03 22:31:59 2010 +0200
@@ -335,7 +335,6 @@
\indexdef{}{ML}{Isar.loop}\verb|Isar.loop: unit -> unit| \\
\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 ->|\isasep\isanewline%
\verb| {context: Proof.context, facts: thm list, goal: thm}| \\
\end{mldecls}
@@ -352,9 +351,6 @@
toplevel state and error condition, respectively. This only works
after having dropped out of the Isar toplevel loop.
- \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 ()| produces the full Isar goal state,
consisting of proof context, facts that have been indicated for
immediate use, and the tactical goal according to