# HG changeset patch
# User wenzelm
# Date 863630879 -7200
# Node ID 50f42a1d7fb9c868b607fd7b4c69afe3941b517b
# Parent  445555a7b714ff498366538d916721dfcd84cf2f
SYNC;

diff -r 445555a7b714 -r 50f42a1d7fb9 doc-src/System/system.ind
--- a/doc-src/System/system.ind	Wed May 14 19:27:21 1997 +0200
+++ b/doc-src/System/system.ind	Wed May 14 19:27:59 1997 +0200
@@ -1,10 +1,10 @@
 \begin{theindex}
 
-  \item browser, \bold{14}
+  \item browser, \bold{13}
 
   \indexspace
 
-  \item {\tt finish_html}, \bold{11}
+  \item {\tt finish_html}, \bold{10}
 
   \indexspace
 
@@ -12,11 +12,11 @@
 
   \indexspace
 
-  \item HTML, \bold{10}
+  \item HTML, \bold{9}
 
   \indexspace
 
-  \item {\tt init_html}, \bold{11}
+  \item {\tt init_html}, \bold{10}
   \item {\tt INSTALL}, 1
   \item {\tt ISABELLE}, 3
   \item {\tt Isabelle}, 1
@@ -29,7 +29,7 @@
 
   \indexspace
 
-  \item {\tt make_html}, \bold{11}
+  \item {\tt make_html}, \bold{10}
 
   \indexspace
 
@@ -37,6 +37,6 @@
 
   \indexspace
 
-  \item {\tt use_dir}, 12
+  \item {\tt use_dir}, 11
 
 \end{theindex}