diff -r 7631f6f7873d -r e3c4d1b0b351 NEWS
--- a/NEWS	Sat Apr 21 20:52:33 2012 +0200
+++ b/NEWS	Sat Apr 21 21:38:08 2012 +0200
@@ -674,6 +674,8 @@
     Goals are generalized over all free variables by default; this is
     necessary for variables whose types changes, but can be overridden
     for specific variables with e.g. 'transfer fixing: x y z'.
+    The variant transfer' method allows replacing a subgoal with
+    one that is logically stronger (rather than equivalent).
 
   - relator_eq attribute: Collects identity laws for relators of
     various type constructors, e.g. "list_all2 (op =) = (op =)". The
@@ -729,10 +731,7 @@
 
   - The 'quotient_definition' command now requires the user to prove a
     respectfulness property at the point where the constant is
-    defined, similar to lift_definition; INCOMPATIBILITY. Users are
-    encouraged to use lift_definition + transfer instead of
-    quotient_definition + descending, which will eventually be
-    deprecated.
+    defined, similar to lift_definition; INCOMPATIBILITY.
 
   - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems
     accordingly, INCOMPATIBILITY.