--- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 12 16:07:20 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{simp}%
%
-\isamarkupsubsubsection{Simplification rules%
+\isamarkupsubsubsection{Simplification Rules%
}
%
\begin{isamarkuptext}%
@@ -40,7 +40,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{The simplification method%
+\isamarkupsubsubsection{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%
+\isamarkupsubsubsection{Adding and Deleting Simplification Rules%
}
%
\begin{isamarkuptext}%
@@ -126,7 +126,7 @@
other arguments.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Rewriting with definitions%
+\isamarkupsubsubsection{Rewriting with Definitions%
}
%
\begin{isamarkuptext}%
@@ -175,7 +175,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Simplifying let-expressions%
+\isamarkupsubsubsection{Simplifying Let-Expressions%
}
%
\begin{isamarkuptext}%
@@ -195,7 +195,7 @@
default:%
\end{isamarkuptext}%
\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
-\isamarkupsubsubsection{Conditional equations%
+\isamarkupsubsubsection{Conditional Equations%
}
%
\begin{isamarkuptext}%
@@ -223,7 +223,7 @@
assumption of the subgoal.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Automatic case splits%
+\isamarkupsubsubsection{Automatic Case Splits%
}
%
\begin{isamarkuptext}%