# HG changeset patch
# User wenzelm
# Date 1136062184 -3600
# Node ID ab3f32f86847dbc704ffb56e27648154b818567c
# Parent  84b0597808bb1f3bd5c9e359d605796b4170f753
* Provers/classical: removed obsolete classical version of elim_format;

diff -r 84b0597808bb -r ab3f32f86847 NEWS
--- a/NEWS	Sat Dec 31 21:49:43 2005 +0100
+++ b/NEWS	Sat Dec 31 21:49:44 2005 +0100
@@ -180,16 +180,20 @@
 * Provers/induct: support coinduction as well.  See
 src/HOL/Library/Coinductive_List.thy for various examples.
 
-* Input syntax now supports dummy variable binding "%_. b", where the
-body does not mention the bound variable.  Note that dummy patterns
-implicitly depend on their context of bounds, which makes "{_. _}"
-match any set comprehension as expected.  Potential INCOMPATIBILITY --
-parse translations need to cope with syntactic constant "_idtdummy" in
-the binding position.
-
-* Removed obsolete syntactic constant "_K" and its associated parse
-translation.  INCOMPATIBILITY -- use dummy abstraction instead, for
-example "A -> B" => "Pi A (%_. B)".
+* Provers/classical: removed obsolete classical version of elim_format
+attribute; classical elim/dest rules are now treated uniformly when
+manipulating the claset.
+
+* Syntax: input syntax now supports dummy variable binding "%_. b",
+where the body does not mention the bound variable.  Note that dummy
+patterns implicitly depend on their context of bounds, which makes
+"{_. _}" match any set comprehension as expected.  Potential
+INCOMPATIBILITY -- parse translations need to cope with syntactic
+constant "_idtdummy" in the binding position.
+
+* Syntax: removed obsolete syntactic constant "_K" and its associated
+parse translation.  INCOMPATIBILITY -- use dummy abstraction instead,
+for example "A -> B" => "Pi A (%_. B)".
 
 
 *** HOL ***