--- a/doc-src/TutorialI/Advanced/document/simp.tex Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
\begin{isabellebody}%
\def\isabellecontext{simp}%
%
-\isamarkupsection{Simplification}
+\isamarkupsection{Simplification%
+}
%
\begin{isamarkuptext}%
\label{sec:simplification-II}\index{simplification|(}
@@ -12,9 +13,11 @@
situation.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Advanced features}
+\isamarkupsubsection{Advanced features%
+}
%
-\isamarkupsubsubsection{Congruence rules}
+\isamarkupsubsubsection{Congruence rules%
+}
%
\begin{isamarkuptext}%
\label{sec:simp-cong}
@@ -75,7 +78,8 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Permutative rewrite rules}
+\isamarkupsubsubsection{Permutative rewrite rules%
+}
%
\begin{isamarkuptext}%
\index{rewrite rule!permutative|bold}
@@ -120,7 +124,8 @@
this.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{How it works}
+\isamarkupsubsection{How it works%
+}
%
\begin{isamarkuptext}%
\label{sec:SimpHow}
@@ -129,7 +134,8 @@
proved (again by simplification). Below we explain some special features of the rewriting process.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Higher-order patterns}
+\isamarkupsubsubsection{Higher-order patterns%
+}
%
\begin{isamarkuptext}%
\index{simplification rule|(}
@@ -167,7 +173,8 @@
sides. They may not contain extraneous term or type variables, though.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{The preprocessor}
+\isamarkupsubsubsection{The preprocessor%
+}
%
\begin{isamarkuptext}%
When some theorem is declared a simplification rule, it need not be a