diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Nov 06 16:41:39 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{simp}%
 %
-\isamarkupsubsubsection{Simplification rules}
+\isamarkupsubsubsection{Simplification rules%
+}
 %
 \begin{isamarkuptext}%
 \indexbold{simplification rule}
@@ -39,7 +40,8 @@
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{The simplification method}
+\isamarkupsubsubsection{The simplification method%
+}
 %
 \begin{isamarkuptext}%
 \index{*simp (method)|bold}
@@ -55,7 +57,8 @@
 Note that \isa{simp} fails if nothing changes.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Adding and deleting simplification rules}
+\isamarkupsubsubsection{Adding and deleting simplification rules%
+}
 %
 \begin{isamarkuptext}%
 If a certain theorem is merely needed in a few proofs by simplification,
@@ -73,7 +76,8 @@
 \end{quote}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Assumptions}
+\isamarkupsubsubsection{Assumptions%
+}
 %
 \begin{isamarkuptext}%
 \index{simplification!with/of assumptions}
@@ -123,7 +127,8 @@
 other arguments.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Rewriting with definitions}
+\isamarkupsubsubsection{Rewriting with definitions%
+}
 %
 \begin{isamarkuptext}%
 \index{simplification!with definitions}
@@ -171,7 +176,8 @@
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Simplifying let-expressions}
+\isamarkupsubsubsection{Simplifying let-expressions%
+}
 %
 \begin{isamarkuptext}%
 \index{simplification!of let-expressions}
@@ -190,7 +196,8 @@
 default:%
 \end{isamarkuptext}%
 \isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
-\isamarkupsubsubsection{Conditional equations}
+\isamarkupsubsubsection{Conditional equations%
+}
 %
 \begin{isamarkuptext}%
 So far all examples of rewrite rules were equations. The simplifier also
@@ -217,7 +224,8 @@
 assumption of the subgoal.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Automatic case splits}
+\isamarkupsubsubsection{Automatic case splits%
+}
 %
 \begin{isamarkuptext}%
 \indexbold{case splits}\index{*split|(}
@@ -310,7 +318,8 @@
 \index{*split|)}%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{Arithmetic}
+\isamarkupsubsubsection{Arithmetic%
+}
 %
 \begin{isamarkuptext}%
 \index{arithmetic}
@@ -330,7 +339,8 @@
 is not proved by simplification and requires \isa{arith}.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Tracing}
+\isamarkupsubsubsection{Tracing%
+}
 %
 \begin{isamarkuptext}%
 \indexbold{tracing the simplifier}