# HG changeset patch
# User wenzelm
# Date 864227484 -7200
# Node ID d95d209ae1c2a21cd41abd4e483d3db7f2d922f2
# Parent  f8bf5e5c1641b0da61cab31e61b740c0b9788cd1
SYNC;

diff -r f8bf5e5c1641 -r d95d209ae1c2 doc-src/System/system.ind
--- a/doc-src/System/system.ind	Wed May 21 17:05:42 1997 +0200
+++ b/doc-src/System/system.ind	Wed May 21 17:11:24 1997 +0200
@@ -1,52 +1,52 @@
 \begin{theindex}
 
-  \item {\tt doc} tool, 7
+  \item {\tt doc} tool, 8
   \item {\tt DVI_VIEWER} setting, 4
 
   \indexspace
 
-  \item {\tt expandshort} tool, 7
+  \item {\tt expandshort} tool, 8
 
   \indexspace
 
-  \item {\tt findlogics} tool, 8
-  \item {\tt finish_html}, \bold{15}
+  \item {\tt findlogics} tool, 9
+  \item {\tt finish_html}, \bold{16}
 
   \indexspace
 
-  \item {\tt getenv} tool, 8
+  \item {\tt getenv} tool, 9
 
   \indexspace
 
-  \item HTML, 9, \bold{14}
+  \item HTML, 11, \bold{15}
 
   \indexspace
 
-  \item {\tt init_html}, \bold{15}
+  \item {\tt init_html}, \bold{16}
   \item {\tt INSTALL}, 1
-  \item {\tt installfonts} tool, 11
+  \item {\tt installfonts} tool, 12
   \item {\tt ISABELLE} setting, 3
-  \item {\tt Isabelle}, 1
+  \item {\tt Isabelle}, 1, 6
   \item {\tt isabelle}, 1, 4
   \item {\tt ISABELLE_DOCS} setting, 4
   \item {\tt ISABELLE_HOME} setting, 2, 3
   \item {\tt ISABELLE_HOME_USER} setting, 3
   \item {\tt ISABELLE_INSTALL_FONTS} setting, 4
-  \item {\tt ISABELLE_INSTALLFONTS} setting, 11
-  \item {\tt ISABELLE_INTERFACE} setting, 4
+  \item {\tt ISABELLE_INSTALLFONTS} setting, 12
+  \item {\tt ISABELLE_INTERFACE} setting, 4, 6
   \item {\tt ISABELLE_LOGIC} setting, 4
   \item {\tt ISABELLE_OUTPUT} setting, 3, 4
   \item {\tt ISABELLE_PATH} setting, 3
   \item {\tt ISABELLE_TOOLS} setting, 4
-  \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 9
-  \item {\tt IsaMakefile}, 9
+  \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 11
+  \item {\tt IsaMakefile}, 10, 11
   \item {\tt ISATOOL} setting, 3
-  \item {\tt isatool}, 1
+  \item {\tt isatool}, 1, 6
 
   \indexspace
 
-  \item {\tt make} tool, 9
-  \item {\tt make_html}, \bold{15}
+  \item {\tt make} tool, 10
+  \item {\tt make_html}, \bold{16}
   \item {\tt ML_HOME} setting, 3
   \item {\tt ML_OPTIONS} setting, 3
   \item {\tt ML_SYSTEM} setting, 3
@@ -54,12 +54,12 @@
   \indexspace
 
   \item settings, \bold{1}
-  \item {\tt symbolinput} tool, 12
-  \item {\tt symbols}, 11
+  \item {\tt symbolinput} tool, 13
+  \item {\tt symbols}, 12
 
   \indexspace
 
-  \item {\tt use_dir}, 10, 15, 16
-  \item {\tt usedir} tool, 9
+  \item {\tt use_dir}, 11, 16, 17
+  \item {\tt usedir} tool, 10
 
 \end{theindex}