more sections;

--- a/src/Pure/Thy/browser_info.ML	Wed Sep 29 13:49:27 1999 +0200
+++ b/src/Pure/Thy/browser_info.ML	Wed Sep 29 13:49:49 1999 +0200
@@ -22,6 +22,8 @@
   val results: string -> string -> thm list -> unit
   val theorem: string -> thm -> unit
   val theorems: string -> thm list -> unit
+  val subsection: string -> unit
+  val subsubsection: string -> unit
   val setup: (theory -> theory) list
 end;
 
@@ -367,6 +369,8 @@
 fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm));
 fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms));
 fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
+fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s));
+fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s));
 
 
 

--- 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";