NEWS
changeset 57882 38bf4de248a6
parent 57737 72d4c00064af
parent 57869 9665f79a7181
child 57941 57200bdc2aa7
     1.1 --- a/NEWS	Sun Aug 10 14:31:06 2014 +0200
     1.2 +++ b/NEWS	Sun Aug 10 14:34:43 2014 +0200
     1.3 @@ -97,6 +97,9 @@
     1.4  handling and propagation to enclosing text area -- avoid loosing
     1.5  keystrokes with slow / remote graphics displays.
     1.6  
     1.7 +* Completion popup supports both ENTER and TAB (default) to select an
     1.8 +item, depending on Isabelle options.
     1.9 +
    1.10  * Refined insertion of completion items wrt. jEdit text: multiple
    1.11  selections, rectangular selections, rectangular selection as "tall
    1.12  caret".
    1.13 @@ -120,6 +123,11 @@
    1.14  * More support for remote files (e.g. http) using standard Java
    1.15  networking operations instead of jEdit virtual file-systems.
    1.16  
    1.17 +* Empty editors buffers that are no longer required (e.g.\ via theory
    1.18 +imports) are automatically removed from the document model.
    1.19 +
    1.20 +* Improved monitor panel.
    1.21 +
    1.22  * Improved Console/Scala plugin: more uniform scala.Console output,
    1.23  more robust treatment of threads and interrupts.
    1.24  
    1.25 @@ -357,6 +365,42 @@
    1.26  
    1.27  INCOMPATIBILITY.
    1.28  
    1.29 +* Lifting and Transfer:
    1.30 +  - a type variable as a raw type is supported
    1.31 +  - stronger reflexivity prover
    1.32 +  - rep_eq is always generated by lift_definition
    1.33 +  - setup for Lifting/Transfer is now automated for BNFs
    1.34 +    + holds for BNFs that do not contain a dead variable
    1.35 +    + relator_eq, relator_mono, relator_distr, relator_domain,
    1.36 +      relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
    1.37 +      right_unique, right_total, left_unique, left_total are proved
    1.38 +      automatically
    1.39 +    + definition of a predicator is generated automatically
    1.40 +    + simplification rules for a predicator definition are proved
    1.41 +      automatically for datatypes
    1.42 +  - consolidation of the setup of Lifting/Transfer
    1.43 +    + property that a relator preservers reflexivity is not needed any
    1.44 +      more
    1.45 +      Minor INCOMPATIBILITY.
    1.46 +    + left_total and left_unique rules are now transfer rules
    1.47 +      (reflexivity_rule attribute not needed anymore)
    1.48 +      INCOMPATIBILITY.
    1.49 +    + Domainp does not have to be a separate assumption in
    1.50 +      relator_domain theorems (=> more natural statement)
    1.51 +      INCOMPATIBILITY.
    1.52 +  - registration of code equations is more robust
    1.53 +    Potential INCOMPATIBILITY.
    1.54 +  - respectfulness proof obligation is preprocessed to a more readable
    1.55 +    form
    1.56 +    Potential INCOMPATIBILITY.
    1.57 +  - eq_onp is always unfolded in respectfulness proof obligation
    1.58 +    Potential INCOMPATIBILITY.
    1.59 +  - unregister lifting setup for Code_Numeral.integer and
    1.60 +    Code_Numeral.natural
    1.61 +    Potential INCOMPATIBILITY.
    1.62 +  - Lifting.invariant -> eq_onp
    1.63 +    INCOMPATIBILITY.
    1.64 +
    1.65  * New internal SAT solver "cdclite" that produces models and proof
    1.66  traces.  This solver replaces the internal SAT solvers "enumerate" and
    1.67  "dpll".  Applications that explicitly used one of these two SAT
    1.68 @@ -776,6 +820,9 @@
    1.69  * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
    1.70  is subsumed by session Kleene_Algebra in AFP.
    1.71  
    1.72 +* HOL-Library / theory RBT: various constants and facts are hidden;
    1.73 +lifting setup is unregistered.  INCOMPATIBILITY.
    1.74 +
    1.75  * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
    1.76  
    1.77  * HOL-Word: bit representations prefer type bool over type bit.
    1.78 @@ -868,6 +915,13 @@
    1.79      bounded_linear_imp_linear ~>  bounded_linear.linear
    1.80  
    1.81  * HOL-Probability:
    1.82 +  - Renamed positive_integral to nn_integral:
    1.83 +
    1.84 +    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
    1.85 +      positive_integral_positive ~> nn_integral_nonneg
    1.86 +
    1.87 +    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
    1.88 +
    1.89    - replaced the Lebesgue integral on real numbers by the more general
    1.90      Bochner integral for functions into a real-normed vector space.
    1.91  
    1.92 @@ -882,14 +936,14 @@
    1.93      integrable_nonneg           ~>  integrableI_nonneg
    1.94      integral_positive           ~>  integral_nonneg_AE
    1.95      integrable_abs_iff          ~>  integrable_abs_cancel
    1.96 -    positive_integral_lim_INF   ~>  positive_integral_liminf
    1.97 +    positive_integral_lim_INF   ~>  nn_integral_liminf
    1.98      lebesgue_real_affine        ~>  lborel_real_affine
    1.99      borel_integral_has_integral ~>  has_integral_lebesgue_integral
   1.100      integral_indicator          ~>
   1.101           integral_real_indicator / integrable_real_indicator
   1.102 -    positive_integral_fst       ~>  positive_integral_fst'
   1.103 -    positive_integral_fst_measurable ~> positive_integral_fst
   1.104 -    positive_integral_snd_measurable ~> positive_integral_snd
   1.105 +    positive_integral_fst       ~>  nn_integral_fst'
   1.106 +    positive_integral_fst_measurable ~> nn_integral_fst
   1.107 +    positive_integral_snd_measurable ~> nn_integral_snd
   1.108  
   1.109      integrable_fst_measurable   ~>
   1.110           integral_fst / integrable_fst / AE_integrable_fst
   1.111 @@ -915,7 +969,7 @@
   1.112           integrable_has_integral_lebesgue_nonneg
   1.113  
   1.114      lebesgue_integral_real_affine  ~>
   1.115 -         positive_integral_real_affine
   1.116 +         nn_integral_real_affine
   1.117  
   1.118      has_integral_iff_positive_integral_lborel  ~>
   1.119           integral_has_integral_nonneg / integrable_has_integral_nonneg
   1.120 @@ -930,13 +984,6 @@
   1.121      integral_cmul_indicator
   1.122      integral_real
   1.123  
   1.124 -  - Renamed positive_integral to nn_integral:
   1.125 -
   1.126 -    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
   1.127 -      positive_integral_positive ~> nn_integral_nonneg
   1.128 -
   1.129 -    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
   1.130 -
   1.131    - Formalized properties about exponentially, Erlang, and normal
   1.132      distributed random variables.
   1.133