# HG changeset patch
# User clasohm
# Date 826111156 -3600
# Node ID 4a617e14d12c0afea13cd61ddc302a6aa8502461
# Parent  f945e3a96b3595b709a0b4f6320575573e8c02b9
documented new function 'section'

diff -r f945e3a96b35 -r 4a617e14d12c doc-src/Ref/theories.tex
--- 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}