--- a/doc-src/Ref/theories.tex Wed Mar 06 10:26:43 1996 +0100
+++ b/doc-src/Ref/theories.tex Wed Mar 06 12:19:16 1996 +0100
@@ -524,8 +524,8 @@
\subsection*{Manual HTML generation}
-To manually activate and deactivate the generation of HTML files the
-following commands and reference variables are used:
+To manually control the generation of HTML files the following
+commands and reference variables are used:
\begin{ttbox}
init_html : unit -> unit
@@ -617,6 +617,17 @@
or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
is a hypertext link to the whole \ML{} file.
+You can add section headings to the list of theorems by using
+
+\begin{ttbox}\index{use_dir}
+section: string -> unit
+\end{ttbox}
+
+in a theory's ML file, which converts a plain string to a HTML
+heading and inserts it before the next theorem proved or stored with
+one of the above functions. If {\tt make_html} is {\tt false} nothing
+is done.
+
\subsection*{Using someone else's database}