1.1 --- a/NEWS	Sat May 22 16:46:18 2010 -0700
     1.2 +++ b/NEWS	Sat May 22 17:44:12 2010 -0700
     1.3 @@ -476,6 +476,10 @@
     1.4    foo_unfold ~> foo.unfold
     1.5    foo_induct ~> foo.induct
     1.6  
     1.7 +* The "fixrec_simp" attribute has been removed.  The "fixrec_simp"
     1.8 +method and internal fixrec proofs now use the default simpset instead.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * The "contlub" predicate has been removed.  Proof scripts should use
    1.12  lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.
    1.13