chapter;

--- a/src/Pure/Thy/html.ML	Wed Jan 05 11:37:44 2000 +0100
+++ b/src/Pure/Thy/html.ML	Wed Jan 05 11:38:48 2000 +0100
@@ -37,6 +37,7 @@
   val results: string -> string -> thm list -> text
   val theorem: string -> thm -> text
   val theorems: string -> thm list -> text
+  val chapter: string -> text
   val section: string -> text
   val subsection: string -> text
   val subsubsection: string -> text
@@ -271,6 +272,7 @@
 
 (* sections *)
 
+fun chapter heading = "\n\n<h1>" ^ plain heading ^ "</h1>\n";
 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";

--- a/src/Pure/Thy/present.ML	Wed Jan 05 11:37:44 2000 +0100
+++ b/src/Pure/Thy/present.ML	Wed Jan 05 11:38:48 2000 +0100
@@ -27,6 +27,7 @@
   val results: string -> string -> thm list -> unit
   val theorem: string -> thm -> unit
   val theorems: string -> thm list -> unit
+  val chapter: string -> unit
   val subsection: string -> unit
   val subsubsection: string -> unit
   val setup: (theory -> theory) list
@@ -427,6 +428,7 @@
 fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms));
 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 chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s));
 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));