NEWS

 
 * Refined GUI popup for completion: more robust key/mouse event
 handling and propagation to enclosing text area -- avoid loosing
 keystrokes with slow / remote graphics displays.
 
+* Completion popup supports both ENTER and TAB (default) to select an
+item, depending on Isabelle options.
+
 * Refined insertion of completion items wrt. jEdit text: multiple
 selections, rectangular selections, rectangular selection as "tall
 caret".
 
 * Integrated spell-checker for document text, comments etc. with

 process, without requiring old-fashioned command-line invocation of
 "isabelle jedit -m MODE".
 
 * More support for remote files (e.g. http) using standard Java
 networking operations instead of jEdit virtual file-systems.
+
+* Empty editors buffers that are no longer required (e.g.\ via theory
+imports) are automatically removed from the document model.
+
+* Improved monitor panel.
 
 * Improved Console/Scala plugin: more uniform scala.Console output,
 more robust treatment of threads and interrupts.
 
 * Improved management of dockable windows: clarified keyboard focus

     fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")
     cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")
     vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")
 
 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
 solvers should use "cdclite" instead. In addition, "cdclite" is now

 * HOL-Library: new theory src/HOL/Library/Tree.thy.
 
 * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
 is subsumed by session Kleene_Algebra in AFP.
 
+* 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.
 
 * HOL-Word: bit representations prefer type bool over type bit.
 INCOMPATIBILITY.
 

     derivative_linear         ~>  has_derivative_bounded_linear
     derivative_is_linear      ~>  has_derivative_linear
     bounded_linear_imp_linear ~>  bounded_linear.linear
 
 * HOL-Probability:
+  - Renamed positive_integral to nn_integral:
+
+    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
+      positive_integral_positive ~> nn_integral_nonneg
+
+    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
+
   - replaced the Lebesgue integral on real numbers by the more general
     Bochner integral for functions into a real-normed vector space.
 
     integral_zero               ~>  integral_zero / integrable_zero
     integral_minus              ~>  integral_minus / integrable_minus

     integral_cmult              ~>  integral_mult_right / integrable_mult_right
     integral_triangle_inequality~>  integral_norm_bound
     integrable_nonneg           ~>  integrableI_nonneg
     integral_positive           ~>  integral_nonneg_AE
     integrable_abs_iff          ~>  integrable_abs_cancel
-    positive_integral_lim_INF   ~>  positive_integral_liminf
+    positive_integral_lim_INF   ~>  nn_integral_liminf
     lebesgue_real_affine        ~>  lborel_real_affine
     borel_integral_has_integral ~>  has_integral_lebesgue_integral
     integral_indicator          ~>
          integral_real_indicator / integrable_real_indicator
-    positive_integral_fst       ~>  positive_integral_fst'
-    positive_integral_fst_measurable ~> positive_integral_fst
-    positive_integral_snd_measurable ~> positive_integral_snd
+    positive_integral_fst       ~>  nn_integral_fst'
+    positive_integral_fst_measurable ~> nn_integral_fst
+    positive_integral_snd_measurable ~> nn_integral_snd
 
     integrable_fst_measurable   ~>
          integral_fst / integrable_fst / AE_integrable_fst
 
     integrable_snd_measurable   ~>

     positive_integral_lebesgue_has_integral  ~>
          integral_has_integral_lebesgue_nonneg /
          integrable_has_integral_lebesgue_nonneg
 
     lebesgue_integral_real_affine  ~>
-         positive_integral_real_affine
+         nn_integral_real_affine
 
     has_integral_iff_positive_integral_lborel  ~>
          integral_has_integral_nonneg / integrable_has_integral_nonneg
 
     The following theorems where removed:

     lebesgue_integral_cmult
     lebesgue_integral_multc
     lebesgue_integral_cmult_nonneg
     integral_cmul_indicator
     integral_real
-
-  - Renamed positive_integral to nn_integral:
-
-    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
-      positive_integral_positive ~> nn_integral_nonneg
-
-    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
 
   - Formalized properties about exponentially, Erlang, and normal
     distributed random variables.
 
 * HOL-Decision_Procs: Separate command 'approximate' for approximative