# HG changeset patch
# User bulwahn
# Date 1294765175 -3600
# Node ID c86889cf295be485846dc722678d5da1eb0970db
# Parent  2aec4b8cd289309ab08e7b21e32ffeb598b7f992
NEWS

diff -r 2aec4b8cd289 -r c86889cf295b NEWS
--- a/NEWS	Tue Jan 11 17:38:03 2011 +0100
+++ b/NEWS	Tue Jan 11 17:59:35 2011 +0100
@@ -133,6 +133,12 @@
 
 *** HOL ***
 
+* New simproc that rewrites list comprehensions applied to List.set
+to set comprehensions.
+To deactivate the simproc for historic proof scripts, use:
+  
+  [[simproc del: list_to_set_comprehension]]
+
 * Functions can be declared as coercions and type inference will add
 them as necessary upon input of a term. In theory Complex_Main,
 real :: nat => real and real :: int => real are declared as