--- a/NEWS Sat Apr 21 20:52:33 2012 +0200
+++ b/NEWS Sat Apr 21 21:38:08 2012 +0200
@@ -674,6 +674,8 @@
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'.
+ The variant transfer' method allows replacing a subgoal with
+ one that is logically stronger (rather than equivalent).
- relator_eq attribute: Collects identity laws for relators of
various type constructors, e.g. "list_all2 (op =) = (op =)". The
@@ -729,10 +731,7 @@
- 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.
+ defined, similar to lift_definition; INCOMPATIBILITY.
- Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems
accordingly, INCOMPATIBILITY.