diff -r 0e86aab627f3 -r 5072d6c77baa doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Jun 02 23:38:22 2008 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Jun 02 23:38:24 2008 +0200
@@ -58,6 +58,7 @@
 
 text {*
   \begin{matharray}{rcl}
+    @{command_def "header"} & : & \isarkeep{toplevel} \\[0.5ex]
     @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\
     @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\
     @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\
@@ -79,12 +80,18 @@
   \begin{rail}
     ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
     ;
-    ('text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
+    ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
     ;
   \end{rail}
 
   \begin{descr}
 
+  \item [@{command "header"}~@{text "text"}] provides plain text
+  markup just preceding the formal beginning of a theory.  In actual
+  document preparation the corresponding {\LaTeX} macro @{verbatim
+  "\\isamarkupheader"} may be redefined to produce chapter or section
+  headings.  See also \secref{sec:markup} for further markup commands.
+  
   \item [@{command "chapter"}, @{command "section"}, @{command
   "subsection"}, and @{command "subsubsection"}] mark chapter and
   section headings.