doc-src/IsarImplementation/implementation.tex

--- a/doc-src/IsarImplementation/implementation.tex	Fri Oct 22 20:43:48 2010 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Fri Oct 22 20:51:45 2010 +0100
@@ -94,9 +94,6 @@
 \input{Thy/document/Local_Theory.tex}
 \input{Thy/document/Integration.tex}
 
-\appendix
-\input{Thy/document/ML_old.tex}
-
 \begingroup
 \tocentry{\bibname}
 \bibliographystyle{abbrv} \small\raggedright\frenchspacing