# HG changeset patch
# User paulson
# Date 852628627 -3600
# Node ID 57109c1a653d3002a8bbf3f157f86b49f3603322
# Parent  adbd622bb375f2ea53572e24b1093d6d293c4214
Updated account of implicit simpsets and clasets

diff -r adbd622bb375 -r 57109c1a653d doc-src/Ref/classical.tex
--- 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
diff -r adbd622bb375 -r 57109c1a653d doc-src/Ref/simplifier.tex
--- 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