diff -r 2b658e50683a -r e5324b8b4df5 doc-src/IsarImplementation/Thy/document/Integration.tex
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Mon Feb 16 21:39:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Mon Feb 16 21:39:52 2009 +0100
@@ -158,7 +158,7 @@
   Internally, Isar commands are put together from an empty transition
   extended by name and source position (and optional source text).  It
   is then left to the individual command parser to turn the given
-  concrete syntax into a suitable transition transformer that adjoin
+  concrete syntax into a suitable transition transformer that adjoins
   actual operations on a theory or proof state etc.%
 \end{isamarkuptext}%
 \isamarkuptrue%