src/Pure/Thy/ROOT.ML

--- a/src/Pure/Thy/ROOT.ML	Wed Oct 06 00:33:53 1999 +0200
+++ b/src/Pure/Thy/ROOT.ML	Wed Oct 06 00:34:48 1999 +0200
@@ -21,4 +21,5 @@
 use "latex.ML";
 use "present.ML";
 
+(*theorem database -- user-level interface*)
 use "thm_database.ML";