obsolete;
authorwenzelm
Sun Nov 02 16:50:42 2014 +0100 (2014-11-02)
changeset 58873db866dc081f8
parent 58872 f0f623005324
child 58874 7172c7ffb047
obsolete;
src/Doc/How_to_Prove_it/document/prelude.tex
     1.1 --- a/src/Doc/How_to_Prove_it/document/prelude.tex	Sun Nov 02 16:47:45 2014 +0100
     1.2 +++ b/src/Doc/How_to_Prove_it/document/prelude.tex	Sun Nov 02 16:50:42 2014 +0100
     1.3 @@ -33,7 +33,6 @@
     1.4  \newcommand{\indexdef}[3]%
     1.5  {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
     1.6  
     1.7 -\renewcommand{\isamarkupheader}[1]{{\rmfamily\subsection{#1}}}
     1.8  \renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}}
     1.9  \renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}}
    1.10  % isabelle in-text command font