# HG changeset patch
# User huffman
# Date 1274575452 25200
# Node ID dd47971b987565c252ba69f9233969d86ad802cd
# Parent  3a7c2c949320aa8119cb984dbf74e13de10e0aa0
NEWS: removed fixrec_simp attribute

diff -r 3a7c2c949320 -r dd47971b9875 NEWS
--- a/NEWS	Sat May 22 16:46:18 2010 -0700
+++ b/NEWS	Sat May 22 17:44:12 2010 -0700
@@ -476,6 +476,10 @@
   foo_unfold ~> foo.unfold
   foo_induct ~> foo.induct
 
+* The "fixrec_simp" attribute has been removed.  The "fixrec_simp"
+method and internal fixrec proofs now use the default simpset instead.
+INCOMPATIBILITY.
+
 * The "contlub" predicate has been removed.  Proof scripts should use
 lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.