doc-src/IsarImplementation/Thy/document/integration.tex
changeset 20064 92aad017b847
parent 20027 413d4224269b
child 20447 5b75f1c4d7d6
--- 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}%