diff -r 838077e40a46 -r c326808da921 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Wed Sep 29 13:49:27 1999 +0200
+++ b/src/Pure/Thy/html.ML	Wed Sep 29 13:49:49 1999 +0200
@@ -37,6 +37,8 @@
   val theorem: string -> thm -> text
   val theorems: string -> thm list -> text
   val section: string -> text
+  val subsection: string -> text
+  val subsubsection: string -> text
   val setup: (theory -> theory) list
 end;
 
@@ -266,9 +268,11 @@
 end;
 
 
-(* section *)
+(* sections *)
 
 fun section heading = "\n\n<h2>" ^ plain heading ^ "</h2>\n";
+fun subsection heading = "\n\n<h3>" ^ plain heading ^ "</h3>\n";
+fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";