--- 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}%