# HG changeset patch
# User kuncar
# Date 1406731494 -7200
# Node ID a01caa7145d48c3c35ee1b2330f87d5925a4386c
# Parent  58f46c678352dac8f066d5f1c83726fbe2aa4cbd
NEWS

diff -r 58f46c678352 -r a01caa7145d4 NEWS
--- 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.