diff -r aeb5c72dd72a -r 3b3cc0cf533f doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Mar 19 12:38:36 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Mar 19 13:05:56 2001 +0100
@@ -2,7 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{simp}%
 %
-\isamarkupsubsubsection{Simplification Rules%
+\isamarkupsubsection{Simplification Rules%
 }
 %
 \begin{isamarkuptext}%
@@ -40,7 +40,7 @@
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{The Simplification Method%
+\isamarkupsubsection{The Simplification Method%
 }
 %
 \begin{isamarkuptext}%
@@ -57,7 +57,7 @@
 Note that \isa{simp} fails if nothing changes.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Adding and Deleting Simplification Rules%
+\isamarkupsubsection{Adding and Deleting Simplification Rules%
 }
 %
 \begin{isamarkuptext}%
@@ -76,7 +76,7 @@
 \end{quote}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Assumptions%
+\isamarkupsubsection{Assumptions%
 }
 %
 \begin{isamarkuptext}%
@@ -136,7 +136,7 @@
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Rewriting with Definitions%
+\isamarkupsubsection{Rewriting with Definitions%
 }
 %
 \begin{isamarkuptext}%
@@ -186,7 +186,7 @@
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Simplifying {\tt\slshape let}-Expressions%
+\isamarkupsubsection{Simplifying {\tt\slshape let}-Expressions%
 }
 %
 \begin{isamarkuptext}%
@@ -206,7 +206,7 @@
 default:%
 \end{isamarkuptext}%
 \isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
-\isamarkupsubsubsection{Conditional Equations%
+\isamarkupsubsection{Conditional Equations%
 }
 %
 \begin{isamarkuptext}%
@@ -234,7 +234,7 @@
 assumption of the subgoal.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Automatic Case Splits%
+\isamarkupsubsection{Automatic Case Splits%
 }
 %
 \begin{isamarkuptext}%
@@ -330,7 +330,7 @@
 \end{warn}\index{*split (method, attr.)|)}%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{Arithmetic%
+\isamarkupsubsection{Arithmetic%
 }
 %
 \begin{isamarkuptext}%
@@ -351,7 +351,7 @@
 is not proved by simplification and requires \isa{arith}.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Tracing%
+\isamarkupsubsection{Tracing%
 }
 %
 \begin{isamarkuptext}%