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