1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Jun 02 23:38:22 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Jun 02 23:38:24 2008 +0200
     1.3 @@ -58,6 +58,7 @@
     1.4  
     1.5  text {*
     1.6    \begin{matharray}{rcl}
     1.7 +    @{command_def "header"} & : & \isarkeep{toplevel} \\[0.5ex]
     1.8      @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\
     1.9      @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\
    1.10      @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\
    1.11 @@ -79,12 +80,18 @@
    1.12    \begin{rail}
    1.13      ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
    1.14      ;
    1.15 -    ('text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
    1.16 +    ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
    1.17      ;
    1.18    \end{rail}
    1.19  
    1.20    \begin{descr}
    1.21  
    1.22 +  \item [@{command "header"}~@{text "text"}] provides plain text
    1.23 +  markup just preceding the formal beginning of a theory.  In actual
    1.24 +  document preparation the corresponding {\LaTeX} macro @{verbatim
    1.25 +  "\\isamarkupheader"} may be redefined to produce chapter or section
    1.26 +  headings.  See also \secref{sec:markup} for further markup commands.
    1.27 +  
    1.28    \item [@{command "chapter"}, @{command "section"}, @{command
    1.29    "subsection"}, and @{command "subsubsection"}] mark chapter and
    1.30    section headings.