--- a/NEWS Sun Aug 10 14:31:06 2014 +0200
+++ b/NEWS Sun Aug 10 14:34:43 2014 +0200
@@ -97,6 +97,9 @@
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".
@@ -120,6 +123,11 @@
* 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.
@@ -357,6 +365,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
@@ -776,6 +820,9 @@
* 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.
@@ -868,6 +915,13 @@
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.
@@ -882,14 +936,14 @@
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
@@ -915,7 +969,7 @@
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
@@ -930,13 +984,6 @@
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.