author ballarin Wed, 30 Apr 2003 18:30:57 +0200 changeset 13938 b033b53d0c1e parent 13937 e9d57517c9b1 child 13939 b3ef90abbd02
Simplifier: congruence rule update.
 NEWS file | annotate | diff | comparison | revisions doc-src/Ref/simplifier.tex file | annotate | diff | comparison | revisions
--- 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
--- 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}