1.1 --- a/NEWS	Tue Jul 29 17:13:25 2014 +0200
     1.2 +++ b/NEWS	Wed Jul 30 16:44:54 2014 +0200
     1.3 @@ -348,6 +348,42 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Lifting and Transfer:
     1.8 +  - a type variable as a raw type is supported
     1.9 +  - stronger reflexivity prover
    1.10 +  - rep_eq is always generated by lift_definition
    1.11 +  - setup for Lifting/Transfer is now automated for BNFs 
    1.12 +    + holds for BNFs that do not contain a dead variable
    1.13 +    + relator_eq, relator_mono, relator_distr, relator_domain, 
    1.14 +      relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
    1.15 +      right_unique, right_total, left_unique, left_total are proved
    1.16 +      automatically
    1.17 +    + definition of a predicator is generated automatically
    1.18 +    + simplification rules for a predicator definition are proved
    1.19 +      automatically for datatypes
    1.20 +  - consolidation of the setup of Lifting/Transfer
    1.21 +    + property that a relator preservers reflexivity is not needed any 
    1.22 +      more
    1.23 +      Minor INCOMPATIBILITY.
    1.24 +    + left_total and left_unique rules are now transfer rules 
    1.25 +      (reflexivity_rule attribute not needed anymore)
    1.26 +      INCOMPATIBILITY.
    1.27 +    + Domainp does not have to be a separate assumption in 
    1.28 +      relator_domain theorems (=> more natural statement)
    1.29 +      INCOMPATIBILITY.
    1.30 +  - registration of code equations is more robust
    1.31 +    Potential INCOMPATIBILITY.
    1.32 +  - respectfulness proof obligation is preprocessed to a more readable
    1.33 +    form
    1.34 +    Potential INCOMPATIBILITY.
    1.35 +  - eq_onp is always unfolded in respectfulness proof obligation
    1.36 +    Potential INCOMPATIBILITY.
    1.37 +  - unregister lifting setup for Code_Numeral.integer and 
    1.38 +    Code_Numeral.natural
    1.39 +    Potential INCOMPATIBILITY.
    1.40 +  - Lifting.invariant -> eq_onp
    1.41 +    INCOMPATIBILITY.
    1.42 +    
    1.43  * New internal SAT solver "cdclite" that produces models and proof
    1.44  traces.  This solver replaces the internal SAT solvers "enumerate" and
    1.45  "dpll".  Applications that explicitly used one of these two SAT
    1.46 @@ -767,6 +803,10 @@
    1.47  * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
    1.48  is subsumed by session Kleene_Algebra in AFP.
    1.49  
    1.50 +* HOL-Library: RBT.thy: various constants and facts are hidden; 
    1.51 +  lifting setup is unregistered
    1.52 +  INCOMPATIBILITY.
    1.53 +
    1.54  * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
    1.55  
    1.56  * HOL-Word: bit representations prefer type bool over type bit.