diff -r 911addd19e9f -r c5e1cce7ace3 src/Doc/Tutorial/Documents/Documents.thy --- a/src/Doc/Tutorial/Documents/Documents.thy Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Doc/Tutorial/Documents/Documents.thy Sun Nov 02 15:27:37 2014 +0100 @@ -424,24 +424,6 @@ do not affect the formal meaning of a theory (or proof), but result in corresponding {\LaTeX} elements. - There are separate markup commands depending on the textual context: - in header position (just before \isakeyword{theory}), within the - theory body, or within a proof. The header needs to be treated - specially here, since ordinary theory and proof commands may only - occur \emph{after} the initial \isakeyword{theory} specification. - - \medskip - - \begin{tabular}{llll} - header & theory & proof & default meaning \\\hline - & \commdx{chapter} & & \verb,\chapter, \\ - \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\ - & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\ - & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\ - \end{tabular} - - \medskip - From the Isabelle perspective, each markup command takes a single $text$ argument (delimited by \verb,",~@{text \}~\verb,", or \verb,{,\verb,*,~@{text \}~\verb,*,\verb,},). After stripping any