1.1 --- a/NEWS	Wed May 02 16:56:25 2012 +0200
     1.2 +++ b/NEWS	Wed May 02 17:23:41 2012 +0200
     1.3 @@ -198,7 +198,11 @@
     1.4  produces a rule which can be used to perform case distinction on both
     1.5  a list and a nat.
     1.6  
     1.7 -* New Transfer package:
     1.8 +* Transfer: New package intended to generalize the existing descending
     1.9 +method and related theorem attributes from the Quotient package. (Not
    1.10 +all functionality is implemented yet, but future development will
    1.11 +focus on Transfer as an eventual replacement for the corresponding
    1.12 +parts of the Quotient package.)
    1.13  
    1.14    - transfer_rule attribute: Maintains a collection of transfer rules,
    1.15      which relate constants at two different types. Transfer rules may
    1.16 @@ -213,7 +217,7 @@
    1.17      equivalent subgoal on the corresponding raw types. Constants are
    1.18      replaced with corresponding ones according to the transfer rules.
    1.19      Goals are generalized over all free variables by default; this is
    1.20 -    necessary for variables whose types changes, but can be overridden
    1.21 +    necessary for variables whose types change, but can be overridden
    1.22      for specific variables with e.g. 'transfer fixing: x y z'.  The
    1.23      variant transfer' method allows replacing a subgoal with one that
    1.24      is logically stronger (rather than equivalent).
    1.25 @@ -231,7 +235,8 @@
    1.26    - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer
    1.27      from type nat to type int.
    1.28  
    1.29 -* New Lifting package:
    1.30 +* Lifting: New package intended to generalize the quotient_definition
    1.31 +facility of the Quotient package; designed to work with Transfer.
    1.32  
    1.33    - lift_definition command: Defines operations on an abstract type in
    1.34      terms of a corresponding operation on a representation
    1.35 @@ -259,8 +264,8 @@
    1.36      lift_definition command to work with the type.
    1.37  
    1.38    - Usage examples: See Quotient_Examples/Lift_DList.thy,
    1.39 -    Quotient_Examples/Lift_RBT.thy, Word/Word.thy and
    1.40 -    Library/Float.thy.
    1.41 +    Quotient_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy,
    1.42 +    Word/Word.thy and Library/Float.thy.
    1.43  
    1.44  * Quotient package:
    1.45