--- a/src/Doc/How_to_Prove_it/document/prelude.tex Sun Nov 02 16:47:45 2014 +0100
+++ b/src/Doc/How_to_Prove_it/document/prelude.tex Sun Nov 02 16:50:42 2014 +0100
@@ -33,7 +33,6 @@
\newcommand{\indexdef}[3]%
{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
-\renewcommand{\isamarkupheader}[1]{{\rmfamily\subsection{#1}}}
\renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}}
\renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}}
% isabelle in-text command font