doc-src/TutorialI/Misc/document/simp.tex

 %
 \begin{isabellebody}%
 \def\isabellecontext{simp}%
 %
-\isamarkupsubsubsection{Simplification rules}
+\isamarkupsubsubsection{Simplification rules%
+}
 %
 \begin{isamarkuptext}%
 \indexbold{simplification rule}
 To facilitate simplification, theorems can be declared to be simplification
 rules (with the help of the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp

   to include simplification rules that can lead to nontermination, either on
   their own or in combination with other simplification rules.
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{The simplification method}
+\isamarkupsubsubsection{The simplification method%
+}
 %
 \begin{isamarkuptext}%
 \index{*simp (method)|bold}
 The general format of the simplification method is
 \begin{quote}

 only the first subgoal and may thus need to be repeated---use
 \isaindex{simp_all} to simplify all subgoals.
 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,
 we do not need to make it a global simplification rule. Instead we can modify
 the set of simplification rules used in a simplification step by adding rules

 \begin{quote}
 \isa{only{\isacharcolon}} \textit{list of theorem names}
 \end{quote}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Assumptions}
+\isamarkupsubsubsection{Assumptions%
+}
 %
 \begin{isamarkuptext}%
 \index{simplification!with/of assumptions}
 By default, assumptions are part of the simplification process: they are used
 as simplification rules and are simplified themselves. For example:%

 
 Note that only one of the above options is allowed, and it must precede all
 other arguments.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Rewriting with definitions}
+\isamarkupsubsubsection{Rewriting with definitions%
+}
 %
 \begin{isamarkuptext}%
 \index{simplification!with definitions}
 Constant definitions (\S\ref{sec:ConstDefinitions}) can
 be used as simplification rules, but by default they are not.  Hence the

   occurrences of $f$ with at least two arguments. Thus it is safer to define
   $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Simplifying let-expressions}
+\isamarkupsubsubsection{Simplifying let-expressions%
+}
 %
 \begin{isamarkuptext}%
 \index{simplification!of let-expressions}
 Proving a goal containing \isaindex{let}-expressions almost invariably
 requires the \isa{let}-con\-structs to be expanded at some point. Since

 If, in a particular context, there is no danger of a combinatorial explosion
 of nested \isa{let}s one could even simlify with \isa{Let{\isacharunderscore}def} by
 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
 accepts \emph{conditional} equations, for example%
 \end{isamarkuptext}%

 because the corresponding precondition \isa{rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}
 simplifies to \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}, which is exactly the local
 assumption of the subgoal.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Automatic case splits}
+\isamarkupsubsubsection{Automatic case splits%
+}
 %
 \begin{isamarkuptext}%
 \indexbold{case splits}\index{*split|(}
 Goals containing \isa{if}-expressions are usually proved by case
 distinction on the condition of the \isa{if}. For example the goal%

 \end{warn}
 
 \index{*split|)}%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{Arithmetic}
+\isamarkupsubsubsection{Arithmetic%
+}
 %
 \begin{isamarkuptext}%
 \index{arithmetic}
 The simplifier routinely solves a small class of linear arithmetic formulae
 (over type \isa{nat} and other numeric types): it only takes into account

 \begin{isamarkuptext}%
 \noindent
 is not proved by simplification and requires \isa{arith}.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Tracing}
+\isamarkupsubsubsection{Tracing%
+}
 %
 \begin{isamarkuptext}%
 \indexbold{tracing the simplifier}
 Using the simplifier effectively may take a bit of experimentation.  Set the
 \isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going