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