diff -r bf164c153d10 -r 0de42180febe doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Thu Oct 07 12:39:01 2010 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Thu Oct 07 19:05:42 2010 +0100
@@ -76,6 +76,9 @@
 \listoffigures
 \clearfirst
 
+\setcounter{chapter}{-1}
+
+\input{Thy/document/ML.tex}
 \input{Thy/document/Prelim.tex}
 \input{Thy/document/Logic.tex}
 \input{Thy/document/Tactic.tex}
@@ -86,7 +89,7 @@
 \input{Thy/document/Integration.tex}
 
 \appendix
-\input{Thy/document/ML.tex}
+\input{Thy/document/ML_old.tex}
 
 \begingroup
 \tocentry{\bibname}