Simplifier: congruence rule update.

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