# HG changeset patch
# User wenzelm
# Date 1414943442 -3600
# Node ID db866dc081f88e6f5ae582ce55cc8c4dbb0d4ee1
# Parent  f0f623005324df1fbf3f20b93cffce452bfc543f
obsolete;

diff -r f0f623005324 -r db866dc081f8 src/Doc/How_to_Prove_it/document/prelude.tex
--- 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