Simplifier: congruence rule update.
authorballarin
Wed Apr 30 18:30:57 2003 +0200 (2003-04-30)
changeset 13938b033b53d0c1e
parent 13937 e9d57517c9b1
child 13939 b3ef90abbd02
Simplifier: congruence rule update.
NEWS
doc-src/Ref/simplifier.tex
     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