| changeset 37087 | dd47971b9875 |
| parent 37020 | 6c699a8e6927 |
| child 37143 | 2a5182751151 |
| child 37150 | 73e738371c90 |
--- 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.