diff -r 93d5408eb7d9 -r fbd097aec213 doc-src/TutorialI/Advanced/document/simp.tex
--- a/doc-src/TutorialI/Advanced/document/simp.tex	Sun Oct 21 19:48:19 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/simp.tex	Sun Oct 21 19:49:29 2001 +0200
@@ -1,9 +1,11 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{simp}%
+\isamarkupfalse%
 %
 \isamarkupsection{Simplification%
 }
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \label{sec:simplification-II}\index{simplification|(}
@@ -11,12 +13,15 @@
 outlines the simplification process itself, which can be helpful
 when the simplifier does not do what you expect of it.%
 \end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isamarkupsubsection{Advanced Features%
 }
+\isamarkuptrue%
 %
 \isamarkupsubsubsection{Congruence Rules%
 }
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \label{sec:simp-cong}
@@ -78,9 +83,11 @@
 is occasionally useful but is not a default rule; you have to declare it explicitly.
 \end{warn}%
 \end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isamarkupsubsubsection{Permutative Rewrite Rules%
 }
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \index{rewrite rules!permutative|bold}%
@@ -121,9 +128,11 @@
 necessary because the built-in arithmetic prover often succeeds without
 such tricks.%
 \end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isamarkupsubsection{How the Simplifier Works%
 }
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \label{sec:SimpHow}
@@ -132,9 +141,11 @@
 proved, again by simplification.  Below we explain some special features of
 the rewriting process.%
 \end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isamarkupsubsubsection{Higher-Order Patterns%
 }
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \index{simplification rule|(}
@@ -172,9 +183,11 @@
 There is no restriction on the form of the right-hand
 sides.  They may not contain extraneous term or type variables, though.%
 \end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isamarkupsubsubsection{The Preprocessor%
 }
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \label{sec:simp-preprocessor}
@@ -203,6 +216,8 @@
 \index{simplification rule|)}
 \index{simplification|)}%
 \end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex