author | huffman |

Wed May 02 17:23:41 2012 +0200 (2012-05-02) | |

changeset 47851 | dad2140c2a15 |

parent 47850 | c638127b4653 |

child 47852 | 0c3b8d036a5c |

edit NEWS items for transfer/lifting

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