src/Doc/Tutorial/Documents/Documents.thy

   \medskip The following source fragment illustrates structure markup
   of a theory.  Note that {\LaTeX} labels may be included inside of
   section headings as well.
 
   \begin{ttbox}
-  header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
+  section {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
 
   theory Foo_Bar
   imports Main
   begin
 

   subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
 
   theorem main: \dots
 
   end
-  \end{ttbox}\vspace{-\medskipamount}
-
-  You may occasionally want to change the meaning of markup commands,
-  say via \verb,\renewcommand, in \texttt{root.tex}.  For example,
-  \verb,\isamarkupheader, is a good candidate for some tuning.  We
-  could move it up in the hierarchy to become \verb,\chapter,.
-
-\begin{verbatim}
-  \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
-\end{verbatim}
-
-  \noindent Now we must change the document class given in
-  \texttt{root.tex} to something that supports chapters.  A suitable
-  command is \verb,\documentclass{report},.
-
-  \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
-  hold the name of the current theory context.  This is particularly
-  useful for document headings:
-
-\begin{verbatim}
-  \renewcommand{\isamarkupheader}[1]
-  {\chapter{#1}\markright{THEORY~\isabellecontext}}
-\end{verbatim}
-
-  \noindent Make sure to include something like
-  \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
-  should have more than two pages to show the effect.
+  \end{ttbox}
 *}
 
 
 subsection {* Formal Comments and Antiquotations \label{sec:doc-prep-text} *}