# HG changeset patch
# User wenzelm
# Date 1407167711 -7200
# Node ID 73c683e09401f4c9d8c3ddb189b7d309e3b4a046
# Parent  4a5d335a6fc7653c6cb0021425d6a93188a4569d
tuned;

diff -r 4a5d335a6fc7 -r 73c683e09401 NEWS
--- a/NEWS	Mon Aug 04 17:53:17 2014 +0200
+++ b/NEWS	Mon Aug 04 17:55:11 2014 +0200
@@ -355,9 +355,9 @@
   - 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 
+  - 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, 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
@@ -365,13 +365,13 @@
     + 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 
+    + property that a relator preservers reflexivity is not needed any
       more
       Minor INCOMPATIBILITY.
-    + left_total and left_unique rules are now transfer rules 
+    + 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 
+    + Domainp does not have to be a separate assumption in
       relator_domain theorems (=> more natural statement)
       INCOMPATIBILITY.
   - registration of code equations is more robust
@@ -381,12 +381,12 @@
     Potential INCOMPATIBILITY.
   - eq_onp is always unfolded in respectfulness proof obligation
     Potential INCOMPATIBILITY.
-  - unregister lifting setup for Code_Numeral.integer and 
+  - 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
@@ -806,9 +806,8 @@
 * 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-Library / theory RBT: various constants and facts are hidden;
+lifting setup is unregistered.  INCOMPATIBILITY.
 
 * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.