documented new function 'section'
Wed, 06 Mar 1996 12:19:16 +0100
changeset 1551 4a617e14d12c
parent 1550 f945e3a96b35
child 1552 6f71b5d46700
documented new function 'section'
--- 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:
 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
+section: string -> unit
+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}