--- a/NEWS Tue Jul 29 17:13:25 2014 +0200
+++ b/NEWS Wed Jul 30 16:44:54 2014 +0200
@@ -348,6 +348,42 @@
INCOMPATIBILITY.
+* Lifting and Transfer:
+ - a type variable as a raw type is supported
+ - stronger reflexivity prover
+ - rep_eq is always generated by lift_definition
+ - setup for Lifting/Transfer is now automated for BNFs
+ + holds for BNFs that do not contain a dead variable
+ + relator_eq, relator_mono, relator_distr, relator_domain,
+ relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
+ right_unique, right_total, left_unique, left_total are proved
+ automatically
+ + definition of a predicator is generated automatically
+ + simplification rules for a predicator definition are proved
+ automatically for datatypes
+ - consolidation of the setup of Lifting/Transfer
+ + property that a relator preservers reflexivity is not needed any
+ more
+ Minor INCOMPATIBILITY.
+ + left_total and left_unique rules are now transfer rules
+ (reflexivity_rule attribute not needed anymore)
+ INCOMPATIBILITY.
+ + Domainp does not have to be a separate assumption in
+ relator_domain theorems (=> more natural statement)
+ INCOMPATIBILITY.
+ - registration of code equations is more robust
+ Potential INCOMPATIBILITY.
+ - respectfulness proof obligation is preprocessed to a more readable
+ form
+ Potential INCOMPATIBILITY.
+ - eq_onp is always unfolded in respectfulness proof obligation
+ Potential INCOMPATIBILITY.
+ - unregister lifting setup for Code_Numeral.integer and
+ Code_Numeral.natural
+ Potential INCOMPATIBILITY.
+ - Lifting.invariant -> eq_onp
+ INCOMPATIBILITY.
+
* New internal SAT solver "cdclite" that produces models and proof
traces. This solver replaces the internal SAT solvers "enumerate" and
"dpll". Applications that explicitly used one of these two SAT
@@ -767,6 +803,10 @@
* HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
is subsumed by session Kleene_Algebra in AFP.
+* HOL-Library: RBT.thy: various constants and facts are hidden;
+ lifting setup is unregistered
+ INCOMPATIBILITY.
+
* HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
* HOL-Word: bit representations prefer type bool over type bit.