diff -r 7219a771ab63 -r 9c977f899ebf doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Fri Oct 15 19:54:34 2010 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Fri Oct 15 20:22:56 2010 +0100
@@ -87,9 +87,9 @@
 \input{Thy/document/ML.tex}
 \input{Thy/document/Prelim.tex}
 \input{Thy/document/Logic.tex}
+\input{Thy/document/Syntax.tex}
 \input{Thy/document/Tactic.tex}
 \input{Thy/document/Proof.tex}
-\input{Thy/document/Syntax.tex}
 \input{Thy/document/Isar.tex}
 \input{Thy/document/Local_Theory.tex}
 \input{Thy/document/Integration.tex}