use \tocentry as in implementation manual;
authorwenzelm
Fri, 01 Jun 2012 13:39:14 +0200
changeset 48057 72197611f1e9
parent 48056 396749e9daaf
child 48061 3437685f69fb
use \tocentry as in implementation manual;
doc-src/IsarRef/isar-ref.tex
doc-src/System/system.tex
--- a/doc-src/IsarRef/isar-ref.tex	Fri Jun 01 13:02:09 2012 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Fri Jun 01 13:39:14 2012 +0200
@@ -81,10 +81,12 @@
 \input{Thy/document/ML_Tactic.tex}
 
 \begingroup
+  \tocentry{\bibname}
   \bibliographystyle{abbrv} \small\raggedright\frenchspacing
   \bibliography{../manual}
 \endgroup
 
+\tocentry{\indexname}
 \printindex
 
 \end{document}
--- a/doc-src/System/system.tex	Fri Jun 01 13:02:09 2012 +0200
+++ b/doc-src/System/system.tex	Fri Jun 01 13:39:14 2012 +0200
@@ -35,10 +35,12 @@
 \input{Thy/document/Misc.tex}
 
 \begingroup
+  \tocentry{\bibname}
   \bibliographystyle{abbrv} \small\raggedright\frenchspacing
   \bibliography{../manual}
 \endgroup
 
+\tocentry{\indexname}
 \printindex
 
 \end{document}