# HG changeset patch
# User ballarin
# Date 1051720257 -7200
# Node ID b033b53d0c1eb7a0ee011d8652b7de44e0dd9e0d
# Parent  e9d57517c9b1f880890e6b238f8d46de1882f458
Simplifier: congruence rule update.

diff -r e9d57517c9b1 -r b033b53d0c1e NEWS
--- a/NEWS	Wed Apr 30 17:53:47 2003 +0200
+++ b/NEWS	Wed Apr 30 18:30:57 2003 +0200
@@ -46,6 +46,9 @@
 
   - Accepts free variables as head terms in congruence rules.  Useful in Isar.
 
+  - No longer aborts on failed congruence proof.  Instead, the
+    congruence is ignored.
+
 * Pure: The main goal of the proof state is no longer shown by default, only
 the subgoals. This behaviour is controlled by a new flag.
    PG menu: Isabelle/Isar -> Settings -> Show Main Goal
diff -r e9d57517c9b1 -r b033b53d0c1e doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Wed Apr 30 17:53:47 2003 +0200
+++ b/doc-src/Ref/simplifier.tex	Wed Apr 30 18:30:57 2003 +0200
@@ -624,11 +624,11 @@
 \medskip
 
 \begin{warn}
-  If the simplifier aborts with the message \texttt{Failed congruence
-    proof!}, then the subgoaler or solver has failed to prove a
-  premise of a congruence rule.  This should never occur under normal
-  circumstances; it indicates that some congruence rule, or possibly
-  the subgoaler or solver, is faulty.
+  If a premise of a congruence rule cannot be proved, then the
+  congruence is ignored.  This should only happen if the rule is
+  \emph{conditional} --- that is, contains premises not of the form $t
+  = \Var{x}$; otherwise it indicates that some congruence rule, or
+  possibly the subgoaler or solver, is faulty.
 \end{warn}