diff -r 2203ef9b55ce -r d66b34e46bdf doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Mon Feb 16 20:25:21 2009 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Mon Feb 16 20:47:44 2009 +0100
@@ -1,6 +1,3 @@
-
-%% $Id$
-
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage{latexsym,graphicx}
 \usepackage[refpage]{nomencl}
@@ -71,14 +68,13 @@
 \listoffigures
 \clearfirst
 
-%\input{intro.tex}
-\input{Thy/document/prelim.tex}
-\input{Thy/document/logic.tex}
-\input{Thy/document/tactic.tex}
-\input{Thy/document/proof.tex}
-\input{Thy/document/isar.tex}
-\input{Thy/document/locale.tex}
-\input{Thy/document/integration.tex}
+\input{Thy/document/Prelim.tex}
+\input{Thy/document/Logic.tex}
+\input{Thy/document/Tactic.tex}
+\input{Thy/document/Proof.tex}
+\input{Thy/document/Isar.tex}
+\input{Thy/document/Local_Theory.tex}
+\input{Thy/document/Integration.tex}
 
 \appendix
 \input{Thy/document/ML.tex}