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