--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Mar 19 12:38:36 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Mon Mar 19 13:05:56 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{simp}%
%
-\isamarkupsubsubsection{Simplification Rules%
+\isamarkupsubsection{Simplification Rules%
}
%
\begin{isamarkuptext}%
@@ -40,7 +40,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{The Simplification Method%
+\isamarkupsubsection{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%
+\isamarkupsubsection{Adding and Deleting Simplification Rules%
}
%
\begin{isamarkuptext}%
@@ -76,7 +76,7 @@
\end{quote}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Assumptions%
+\isamarkupsubsection{Assumptions%
}
%
\begin{isamarkuptext}%
@@ -136,7 +136,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Rewriting with Definitions%
+\isamarkupsubsection{Rewriting with Definitions%
}
%
\begin{isamarkuptext}%
@@ -186,7 +186,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Simplifying {\tt\slshape let}-Expressions%
+\isamarkupsubsection{Simplifying {\tt\slshape let}-Expressions%
}
%
\begin{isamarkuptext}%
@@ -206,7 +206,7 @@
default:%
\end{isamarkuptext}%
\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
-\isamarkupsubsubsection{Conditional Equations%
+\isamarkupsubsection{Conditional Equations%
}
%
\begin{isamarkuptext}%
@@ -234,7 +234,7 @@
assumption of the subgoal.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Automatic Case Splits%
+\isamarkupsubsection{Automatic Case Splits%
}
%
\begin{isamarkuptext}%
@@ -330,7 +330,7 @@
\end{warn}\index{*split (method, attr.)|)}%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Arithmetic%
+\isamarkupsubsection{Arithmetic%
}
%
\begin{isamarkuptext}%
@@ -351,7 +351,7 @@
is not proved by simplification and requires \isa{arith}.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Tracing%
+\isamarkupsubsection{Tracing%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Misc/simp.thy Mon Mar 19 12:38:36 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Mon Mar 19 13:05:56 2001 +0100
@@ -2,7 +2,7 @@
theory simp = Main:
(*>*)
-subsubsection{*Simplification Rules*}
+subsection{*Simplification Rules*}
text{*\indexbold{simplification rule}
To facilitate simplification, theorems can be declared to be simplification
@@ -39,7 +39,7 @@
\end{warn}
*}
-subsubsection{*The Simplification Method*}
+subsection{*The Simplification Method*}
text{*\index{*simp (method)|bold}
The general format of the simplification method is
@@ -54,7 +54,7 @@
Note that @{text simp} fails if nothing changes.
*}
-subsubsection{*Adding and Deleting Simplification Rules*}
+subsection{*Adding and Deleting Simplification Rules*}
text{*
If a certain theorem is merely needed in a few proofs by simplification,
@@ -72,7 +72,7 @@
\end{quote}
*}
-subsubsection{*Assumptions*}
+subsection{*Assumptions*}
text{*\index{simplification!with/of assumptions}
By default, assumptions are part of the simplification process: they are used
@@ -133,7 +133,7 @@
\end{warn}
*}
-subsubsection{*Rewriting with Definitions*}
+subsection{*Rewriting with Definitions*}
text{*\index{simplification!with definitions}
Constant definitions (\S\ref{sec:ConstDefinitions}) can
@@ -182,7 +182,7 @@
\end{warn}
*}
-subsubsection{*Simplifying {\tt\slshape let}-Expressions*}
+subsection{*Simplifying {\tt\slshape let}-Expressions*}
text{*\index{simplification!of let-expressions}
Proving a goal containing \isaindex{let}-expressions almost invariably
@@ -203,7 +203,7 @@
*}
declare Let_def [simp]
-subsubsection{*Conditional Equations*}
+subsection{*Conditional Equations*}
text{*
So far all examples of rewrite rules were equations. The simplifier also
@@ -235,7 +235,7 @@
*}
-subsubsection{*Automatic Case Splits*}
+subsection{*Automatic Case Splits*}
text{*\indexbold{case splits}\index{*split (method, attr.)|(}
Goals containing @{text"if"}-expressions are usually proved by case
@@ -338,7 +338,7 @@
by(simp_all)
(*>*)
-subsubsection{*Arithmetic*}
+subsection{*Arithmetic*}
text{*\index{arithmetic}
The simplifier routinely solves a small class of linear arithmetic formulae
@@ -362,7 +362,7 @@
*}
-subsubsection{*Tracing*}
+subsection{*Tracing*}
text{*\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
--- a/doc-src/TutorialI/fp.tex Mon Mar 19 12:38:36 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Mon Mar 19 13:05:56 2001 +0100
@@ -328,7 +328,7 @@
section as well, in particular in order to understand what happened if things
do not simplify as expected.
-\subsubsection{What is Simplification}
+\subsection{What is Simplification}
In its most basic form, simplification means repeated application of
equations from left to right. For example, taking the rules for \isa{\at}