
diff -r 419116f1157a -r e23770bc97c8 doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Thu Feb 26 08:44:44 2009 -0800
+++ b/doc-src/IsarImplementation/implementation.tex	Thu Feb 26 08:48:33 2009 -0800
@@ -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,14 +65,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}
@@ -89,10 +82,6 @@
 \bibliography{../manual}
 \endgroup
 
-%FIXME
-%\tocentry{\glossaryname}
-%\printglossary
-
 \tocentry{\indexname}
 \printindex
 




