--- a/doc-src/Ref/classical.tex Tue Jan 07 09:06:01 1997 +0100
+++ b/doc-src/Ref/classical.tex Tue Jan 07 10:17:07 1997 +0100
@@ -28,10 +28,18 @@
be traced, and their components can be called directly; in this manner,
any proof can be viewed interactively.
-We shall first discuss the underlying principles, then consider how to use
-the classical reasoner. Finally, we shall see how to instantiate it for
-new logics. The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already
-installed.
+The simplest way to apply the classical reasoner (to subgoal~$i$) is as
+follows:
+\begin{ttbox}
+by (Fast_tac \(i\));
+\end{ttbox}
+If the subgoal is a simple formula of the predicate calculus or set theory,
+then it should be proved quickly. However, to use the classical reasoner
+effectively, you need to know how it works.
+
+We shall first discuss the underlying principles, then present the classical
+reasoner. Finally, we shall see how to instantiate it for new logics. The
+logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already installed.
\section{The sequent calculus}
@@ -397,12 +405,12 @@
\end{ttdescription}
\subsection{The current claset}
-Some logics (e.g.\ \HOL) support the concept of a {\em current set of
-classical rules}\index{claset!current}.
-The underlying idea is quite similar to that of a current simpset described
-in \S\ref{sec:simp-for-dummies}.
-Just like simpsets, clasets can be associated with theories.
-The tactics
+Some logics (\FOL, {\HOL} and \ZF) support the concept of a current
+claset\index{claset!current}. This is a default set of classical rules. The
+underlying idea is quite similar to that of a current simpset described in
+\S\ref{sec:simp-for-dummies}; please read that section, including its
+warnings. Just like simpsets, clasets can be associated with theories. The
+tactics
\begin{ttbox}
Step_tac : int -> tactic
Fast_tac : int -> tactic
--- a/doc-src/Ref/simplifier.tex Tue Jan 07 09:06:01 1997 +0100
+++ b/doc-src/Ref/simplifier.tex Tue Jan 07 10:17:07 1997 +0100
@@ -15,17 +15,17 @@
\section{Simplification for dummies}
\label{sec:simp-for-dummies}
-In some logics (e.g.\ \HOL), the simplifier is particularly easy to
-use because it supports the concept of a {\em current set of simplification
- rules}, also called the {\em current simpset}\index{simpset!current}. All
-commands are interpreted relative to the current simpset. For example, in the
-theory of arithmetic the goal
+In some logics (\FOL, {\HOL} and \ZF), the simplifier is particularly easy to
+use because it supports the concept of a {\em current
+ simpset}\index{simpset!current}. This is a default set of simplification
+rules. All commands are interpreted relative to the current simpset. For
+example, in the theory of arithmetic the goal
\begin{ttbox}
{\out 1. 0 + (x + 0) = x + 0 + 0}
\end{ttbox}
can be solved by a single
\begin{ttbox}
-by(Simp_tac 1);
+by (Simp_tac 1);
\end{ttbox}
The simplifier uses the current simpset, which in the case of arithmetic
contains the required theorems $\Var{n}+0 = \Var{n}$ and $0+\Var{n} =
@@ -38,7 +38,7 @@
\end{ttbox}
then there is the more powerful
\begin{ttbox}
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
\end{ttbox}
which solves the above goal.
@@ -117,6 +117,18 @@
designed simpsets need few temporary additions or deletions.
\begin{warn}
+ The union of the ancestor simpsets (as described above) is not always a good
+ simpset for the new theory. If some ancestors have deleted simplification
+ rules because they are no longer wanted, while others have left those rules
+ in, then the union will contain the unwanted rules. If the ancestor
+ simpsets differ in other components (the subgoaler, solver, looper or rule
+ preprocessor: see below), then you cannot be sure which version of that
+ component will be inherited. You may have to set the component explicitly
+ for the new theory's simpset by an assignment of the form
+ {\tt simpset := \dots}.
+\end{warn}
+
+\begin{warn}
If you execute proofs interactively, or load them from an ML file without
associated {\tt .thy} file, you must set the current simpset by calling
\ttindex{set_current_thy}~{\tt"}$T${\tt"}, where $T$ is the name of the
@@ -378,12 +390,12 @@
example
\begin{ttbox}
Addsimps \(thms\);
-by(Simp_tac \(i\));
+by (Simp_tac \(i\));
Delsimps \(thms\);
\end{ttbox}
can be compressed into
\begin{ttbox}
-by(simp_tac (!simpset addsimps \(thms\)) \(i\));
+by (simp_tac (!simpset addsimps \(thms\)) \(i\));
\end{ttbox}
The simpset associated with a particular theory can be retrieved via the name