# HG changeset patch
# User huffman
# Date 1335972221 -7200
# Node ID dad2140c2a1596c659875af6b70f7425b1c0ef90
# Parent  c638127b46537faf1e5f7a32c16fb1218538223d
edit NEWS items for transfer/lifting

diff -r c638127b4653 -r dad2140c2a15 NEWS
--- a/NEWS	Wed May 02 16:56:25 2012 +0200
+++ b/NEWS	Wed May 02 17:23:41 2012 +0200
@@ -198,7 +198,11 @@
 produces a rule which can be used to perform case distinction on both
 a list and a nat.
 
-* New Transfer package:
+* Transfer: New package intended to generalize the existing descending
+method and related theorem attributes from the Quotient package. (Not
+all functionality is implemented yet, but future development will
+focus on Transfer as an eventual replacement for the corresponding
+parts of the Quotient package.)
 
   - transfer_rule attribute: Maintains a collection of transfer rules,
     which relate constants at two different types. Transfer rules may
@@ -213,7 +217,7 @@
     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
+    necessary for variables whose types change, 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).
@@ -231,7 +235,8 @@
   - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer
     from type nat to type int.
 
-* New Lifting package:
+* Lifting: New package intended to generalize the quotient_definition
+facility of the Quotient package; designed to work with Transfer.
 
   - lift_definition command: Defines operations on an abstract type in
     terms of a corresponding operation on a representation
@@ -259,8 +264,8 @@
     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_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy,
+    Word/Word.thy and Library/Float.thy.
 
 * Quotient package: