diff -r f7df7104d13e -r b9e132e54d25 NEWS
--- a/NEWS	Sat Apr 21 13:49:31 2012 +0200
+++ b/NEWS	Sat Apr 21 13:54:29 2012 +0200
@@ -657,6 +657,86 @@
 
 * Theory Library/Multiset: Improved code generation of multisets.
 
+* New Transfer package:
+
+  - transfer_rule attribute: Maintains a collection of transfer rules,
+    which relate constants at two different types. Transfer rules may
+    relate different type instances of the same polymorphic constant,
+    or they may relate an operation on a raw type to a corresponding
+    operation on an abstract type (quotient or subtype). For example:
+
+    ((A ===> B) ===> list_all2 A ===> list_all2 B) map map
+    (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int
+
+  - transfer method: Replaces a subgoal on abstract types with an
+    equivalent subgoal on the corresponding raw types. Constants are
+    replaced with corresponding ones according to the transfer rules.
+    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'.
+
+  - relator_eq attribute: Collects identity laws for relators of
+    various type constructors, e.g. "list_all2 (op =) = (op =)". The
+    transfer method uses these lemmas to infer transfer rules for
+    non-polymorphic constants on the fly.
+
+  - transfer_prover method: Assists with proving a transfer rule for a
+    new constant, provided the constant is defined in terms of other
+    constants that already have transfer rules. It should be applied
+    after unfolding the constant definitions.
+
+  - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer
+    from type nat to type int.
+
+* New Lifting package:
+
+  - lift_definition command: Defines operations on an abstract type in
+    terms of a corresponding operation on a representation type. Example
+    syntax:
+
+    lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist"
+      is List.insert
+
+    Users must discharge a respectfulness proof obligation when each
+    constant is defined. (For a type copy, i.e. a typedef with UNIV,
+    the proof is discharged automatically.) The obligation is
+    presented in a user-friendly, readable form; a respectfulness
+    theorem in the standard format and a transfer rule are generated
+    by the package.
+
+  - Integration with code_abstype: For typedefs (e.g. subtypes
+    corresponding to a datatype invariant, such as dlist),
+    lift_definition generates a code certificate theorem and sets up
+    code generation for each constant.
+
+  - setup_lifting command: Sets up the Lifting package to work with
+    a user-defined type. The user must provide either a quotient
+    theorem or a type_definition theorem. The package configures
+    transfer rules for equality and quantifiers on the type, and sets
+    up the lift_definition command to work with the type.
+
+  - Usage examples: See Quotient_Examples/Lift_DList.thy,
+    Quotient_Examples/Lift_RBT.thy, Word/Word.thy and
+    Library/Float.thy.
+
+* Quotient package:
+
+  - The 'quotient_type' command now supports a 'morphisms' option with
+    rep and abs functions, similar to typedef.
+
+  - 'quotient_type' sets up new types to work with the Lifting and
+    Transfer packages, as with 'setup_lifting'.
+
+  - 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.
+
+  - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems
+    accordingly, INCOMPATIBILITY.
+
 * New diagnostic command 'find_unused_assms' to find potentially
 superfluous assumptions in theorems using Quickcheck.