--- 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}