# HG changeset patch
# User wenzelm
# Date 1338550754 -7200
# Node ID 72197611f1e9e8e1e10c3478d77c7d3390cd4f5a
# Parent  396749e9daafbbc011b0a3b41fc97012e9592791
use \tocentry as in implementation manual;

diff -r 396749e9daaf -r 72197611f1e9 doc-src/IsarRef/isar-ref.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}
diff -r 396749e9daaf -r 72197611f1e9 doc-src/System/system.tex
--- 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}