diff -r 25a3531c0df5 -r b956bf0dc87c doc-src/IsarImplementation/Thy/document/session.tex
--- a/doc-src/IsarImplementation/Thy/document/session.tex	Thu Feb 26 20:57:59 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/session.tex	Thu Feb 26 21:16:53 2009 +0100
@@ -1,21 +1,23 @@
 \input{Base.tex}
 
-\input{Prelim.tex}
-
-\input{Logic.tex}
-
-\input{Tactic.tex}
-
-\input{Proof.tex}
+\input{Integration.tex}
 
 \input{Isar.tex}
 
 \input{Local_Theory.tex}
 
-\input{Integration.tex}
+\input{Logic.tex}
 
 \input{ML.tex}
 
+\input{Prelim.tex}
+
+\input{Proof.tex}
+
+\input{Syntax.tex}
+
+\input{Tactic.tex}
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"