# 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}