# HG changeset patch
# User lcp
# Date 784392431 -3600
# Node ID 23734672dc12c62b53fb23ff75d2ba4a9620b3b6
# Parent  40f72ab196f83018554198506e36036cb1b77b3e
updated discussion of congruence rules in first section

diff -r 40f72ab196f8 -r 23734672dc12 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Wed Nov 09 13:50:59 1994 +0100
+++ b/doc-src/Ref/simplifier.tex	Wed Nov 09 15:47:11 1994 +0100
@@ -69,8 +69,11 @@
 \]
 Given this rule, the simplifier assumes $Q@1$ and extracts rewrite rules
 from it when simplifying~$P@2$.  Such local assumptions are effective for
-rewriting formulae such as $x=0\imp y+x=y$.  The congruence rule for bounded
-quantifiers can also supply contextual information:
+rewriting formulae such as $x=0\imp y+x=y$.  The local assumptions are also
+provided as theorems to the solver; see page~\pageref{sec:simp-solver} below.
+
+Here are some more examples.  The congruence rule for bounded quantifiers
+also supplies contextual information, this time about the bound variable:
 \begin{eqnarray*}
   &&\List{\Var{A}=\Var{B};\; 
           \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\
@@ -83,8 +86,7 @@
          \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
    if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
 \]
-
-A congruence rule can also suppress simplification of certain arguments.
+A congruence rule can also {\em prevent\/} simplification of some arguments.
 Here is an alternative congruence rule for conditional expressions:
 \[ \Var{p}=\Var{q} \Imp
    if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
@@ -121,7 +123,7 @@
 simplification only if that fails; here {\tt prems_of_ss} extracts the
 current premises from a simpset.
 
-\subsection{*The solver}
+\subsection{*The solver}\label{sec:simp-solver}
 The solver is a tactic that attempts to solve a subgoal after
 simplification.  Typically it just proves trivial subgoals such as {\tt
   True} and $t=t$.  It could use sophisticated means such as {\tt
@@ -157,8 +159,8 @@
 \begin{warn}
   If the simplifier aborts with the message {\tt Failed congruence proof!},
   then the subgoaler or solver has failed to prove a premise of a
-  congruence rule.  This should never occur and indicates that the
-  subgoaler or solver is faulty.
+  congruence rule.  This should never occur; it indicates that some
+  congruence rule, or possibly the subgoaler or solver, is faulty.
 \end{warn}