added warning for databases made with set MAKE_HTML
Fri, 26 Jan 1996 12:45:09 +0100
changeset 1452 ee54d2c15d66
parent 1451 6803ecb9b198
child 1453 a4896058a47e
added warning for databases made with set MAKE_HTML
--- a/doc-src/Ref/theories.tex	Tue Jan 23 14:25:55 1996 +0100
+++ b/doc-src/Ref/theories.tex	Fri Jan 26 12:45:09 1996 +0100
@@ -484,6 +484,17 @@
+When using ML databases made this way to load additional theories or
+derive other databases from them, you have to be aware that HTML
+generation remains activated.
+The reason is that the boolean reference variable {\tt make_html} (see
+below) is set. Therefore HTML files are generated unless you assign a
+value of {\tt false} to {\tt make_html}. The only place where the
+environment variable {\tt MAKE_HTML} is used is in the makefile where
+it determines the initial value of {\tt make_html} for a newly made
 As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
 {\tt FOL}) and because the HTML files list a theory's ancestors, you
 should not make HTML files for a logic if the HTML files for the base