--- 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