--- a/NEWS Sun Apr 09 14:20:23 2006 +0200
+++ b/NEWS Sun Apr 09 14:31:37 2006 +0200
@@ -355,20 +355,20 @@
Adaptions may be required in the following cases:
-a) User-defined constants using any of the names "plus", "minus", "times", "less"
-or "less_eq". The standard syntax translations for "+", "-" and "*" may go wrong.
+a) User-defined constants using any of the names "plus", "minus", "times",
+"less" or "less_eq". The standard syntax translations for "+", "-" and "*"
+may go wrong.
INCOMPATIBILITY: use more specific names.
b) Variables named "plus", "minus", "times", "less", "less_eq"
INCOMPATIBILITY: use more specific names.
-c) Commutative equations theorems (e. g. "a + b = b + a")
-Since the changing of names also changes the order of terms, commutative rewrites
-perhaps will be applied when not applied before or the other way round.
-Experience shows that thiis is rarely the case (only two adaptions in the whole
-Isabelle distribution).
-INCOMPATIBILITY: rewrite proof; sometimes already an exchange of a distributive
-law may suffice.
+c) Permutative equations (e.g. "a + b = b + a")
+Since the change of names also changes the order of terms, permutative
+rewrite rules may get applied in a different order. Experience shows that
+this is rarely the case (only two adaptions in the whole Isabelle
+distribution).
+INCOMPATIBILITY: rewrite proofs
d) ML code directly refering to constant names
This in general only affects hand-written proof tactics, simprocs and so on.
@@ -376,6 +376,9 @@
* "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
+* The old set interval syntax "{m..n(}" (and relatives) has been removed.
+ Use "{m..<n}" (and relatives) instead.
+
* In the context of the assumption "~(s = t)" the Simplifier rewrites
"t = s" to False (by simproc "neq_simproc"). For backward
compatibility this can be disabled by ML "reset use_neq_simproc".