diff -r 179ff9cb160b -r 5b25fee0362c doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Wed Mar 04 10:43:39 2009 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Wed Mar 04 10:45:52 2009 +0100
@@ -1,6 +1,3 @@
-
-%% $Id$
-
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage{latexsym,graphicx}
 \usepackage[refpage]{nomencl}
@@ -23,9 +20,6 @@
   and Larry Paulson
 }
 
-%FIXME
-%\makeglossary
-
 \makeindex
 
 
@@ -71,28 +65,24 @@
 \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/Syntax.tex}
+\input{Thy/document/Isar.tex}
+\input{Thy/document/Local_Theory.tex}
+\input{Thy/document/Integration.tex}
 
 \appendix
 \input{Thy/document/ML.tex}
 
 \begingroup
 \tocentry{\bibname}
-\bibliographystyle{plain} \small\raggedright\frenchspacing
+\bibliographystyle{abbrv} \small\raggedright\frenchspacing
 \bibliography{../manual}
 \endgroup
 
-%FIXME
-%\tocentry{\glossaryname}
-%\printglossary
-
 \tocentry{\indexname}
 \printindex