Modified formal of thms in html file.
authornipkow
Thu, 14 Nov 1996 16:01:36 +0100
changeset 2188 6c217c071b97
parent 2187 07c471510cf1
child 2189 c00533aec02f
Modified formal of thms in html file.
src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Nov 14 14:38:51 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML	Thu Nov 14 16:01:36 1996 +0100
@@ -1095,7 +1095,7 @@
       in case !cur_htmlfile of
              Some out =>
                (mk_theorems_title out;
-                output (out, "<EM>" ^ name ^ "</EM>\n<PRE>" ^
+                output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^
                              escape 
 			      (explode 
 			       (string_of_thm (#1 (freeze_thaw thm)))) ^