# HG changeset patch
# User nipkow
# Date 1144585897 -7200
# Node ID 1f717bd6b7eaae6f398b911de9a89a24e9511831
# Parent  529b735edbf29f27bcfb176919f923e846f1c10b
*** empty log message ***

diff -r 529b735edbf2 -r 1f717bd6b7ea NEWS
--- 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".