changeset 29758 | 7a3b5bbed313 |
parent 29755 | d66b34e46bdf |
child 30116 | 1fb1833cb199 |
--- a/doc-src/IsarImplementation/implementation.tex Mon Feb 16 21:04:15 2009 +0100 +++ b/doc-src/IsarImplementation/implementation.tex Mon Feb 16 21:23:33 2009 +0100 @@ -20,9 +20,6 @@ and Larry Paulson } -%FIXME -%\makeglossary - \makeindex @@ -85,10 +82,6 @@ \bibliography{../manual} \endgroup -%FIXME -%\tocentry{\glossaryname} -%\printglossary - \tocentry{\indexname} \printindex