--- a/doc-src/IsarImplementation/Thy/document/integration.tex Sat Jul 08 14:01:31 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Sat Jul 08 14:01:40 2006 +0200
@@ -356,7 +356,7 @@
toplevel state and optional error condition, respectively. This
only works after dropping out of the Isar toplevel loop.
- \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()| above.
+ \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|.
\end{description}%
\end{isamarkuptext}%