author ballarin Wed Apr 30 18:30:57 2003 +0200 (2003-04-30) changeset 13938 b033b53d0c1e parent 13937 e9d57517c9b1 child 13939 b3ef90abbd02
Simplifier: congruence rule update.
 NEWS file | annotate | diff | revisions doc-src/Ref/simplifier.tex file | annotate | diff | revisions
     1.1 --- a/NEWS	Wed Apr 30 17:53:47 2003 +0200
1.2 +++ b/NEWS	Wed Apr 30 18:30:57 2003 +0200
1.3 @@ -46,6 +46,9 @@
1.4
1.5    - Accepts free variables as head terms in congruence rules.  Useful in Isar.
1.6
1.7 +  - No longer aborts on failed congruence proof.  Instead, the
1.8 +    congruence is ignored.
1.9 +
1.10  * Pure: The main goal of the proof state is no longer shown by default, only
1.11  the subgoals. This behaviour is controlled by a new flag.
1.12     PG menu: Isabelle/Isar -> Settings -> Show Main Goal

     2.1 --- a/doc-src/Ref/simplifier.tex	Wed Apr 30 17:53:47 2003 +0200
2.2 +++ b/doc-src/Ref/simplifier.tex	Wed Apr 30 18:30:57 2003 +0200
2.3 @@ -624,11 +624,11 @@
2.4  \medskip
2.5
2.6  \begin{warn}
2.7 -  If the simplifier aborts with the message \texttt{Failed congruence
2.8 -    proof!}, then the subgoaler or solver has failed to prove a
2.9 -  premise of a congruence rule.  This should never occur under normal
2.10 -  circumstances; it indicates that some congruence rule, or possibly
2.11 -  the subgoaler or solver, is faulty.
2.12 +  If a premise of a congruence rule cannot be proved, then the
2.13 +  congruence is ignored.  This should only happen if the rule is
2.14 +  \emph{conditional} --- that is, contains premises not of the form $t 2.15 + = \Var{x}$; otherwise it indicates that some congruence rule, or
2.16 +  possibly the subgoaler or solver, is faulty.
2.17  \end{warn}
2.18
2.19