NEWS
changeset 47856 57d1df2f2a0f
parent 47855 1246d847b8c1
child 47866 2cc26ddd8298
child 47887 4e9c06c194d9
     1.1 --- a/NEWS	Wed May 02 20:31:15 2012 +0200
     1.2 +++ b/NEWS	Wed May 02 20:43:57 2012 +0200
     1.3 @@ -76,15 +76,6 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 -* Discontinued old "prems" fact, which used to refer to the accidental
     1.8 -collection of foundational premises in the context (already marked as
     1.9 -legacy since Isabelle2011).
    1.10 -
    1.11 -* Rule composition via attribute "OF" (or ML functions OF/MRS) is more
    1.12 -tolerant against multiple unifiers, as long as the final result is
    1.13 -unique.  (As before, rules are composed in canonical right-to-left
    1.14 -order to accommodate newly introduced premises.)
    1.15 -
    1.16  * Command 'definition' no longer exports the foundational "raw_def"
    1.17  into the user context.  Minor INCOMPATIBILITY, may use the regular
    1.18  "def" result with attribute "abs_def" to imitate the old version.
    1.19 @@ -94,6 +85,20 @@
    1.20  expand it.  This also works for object-logic equality.  (Formerly
    1.21  undocumented feature.)
    1.22  
    1.23 +* Sort constraints are now propagated in simultaneous statements, just
    1.24 +like type constraints.  INCOMPATIBILITY in rare situations, where
    1.25 +distinct sorts used to be assigned accidentally.  For example:
    1.26 +
    1.27 +  lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"
    1.28 +
    1.29 +  lemma "P (x::'a)" and "Q (y::'a::bar)"
    1.30 +    -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
    1.31 +
    1.32 +* Rule composition via attribute "OF" (or ML functions OF/MRS) is more
    1.33 +tolerant against multiple unifiers, as long as the final result is
    1.34 +unique.  (As before, rules are composed in canonical right-to-left
    1.35 +order to accommodate newly introduced premises.)
    1.36 +
    1.37  * Renamed some inner syntax categories:
    1.38  
    1.39      num ~> num_token
    1.40 @@ -108,8 +113,8 @@
    1.41  "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
    1.42  manual.  Minor INCOMPATIBILITY.
    1.43  
    1.44 -* Obsolete command 'types' has been discontinued.  Use 'type_synonym'
    1.45 -instead.  INCOMPATIBILITY.
    1.46 +* Discontinued configuration option "syntax_positions": atomic terms
    1.47 +in parse trees are always annotated by position constraints.
    1.48  
    1.49  * Old code generator for SML and its commands 'code_module',
    1.50  'code_library', 'consts_code', 'types_code' have been discontinued.
    1.51 @@ -125,17 +130,12 @@
    1.52  
    1.53  INCOMPATIBILITY.
    1.54  
    1.55 -* Sort constraints are now propagated in simultaneous statements, just
    1.56 -like type constraints.  INCOMPATIBILITY in rare situations, where
    1.57 -distinct sorts used to be assigned accidentally.  For example:
    1.58 -
    1.59 -  lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"
    1.60 -
    1.61 -  lemma "P (x::'a)" and "Q (y::'a::bar)"
    1.62 -    -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
    1.63 -
    1.64 -* Discontinued configuration option "syntax_positions": atomic terms
    1.65 -in parse trees are always annotated by position constraints.
    1.66 +* Obsolete 'types' command has been discontinued.  Use 'type_synonym'
    1.67 +instead.  INCOMPATIBILITY.
    1.68 +
    1.69 +* Discontinued old "prems" fact, which used to refer to the accidental
    1.70 +collection of foundational premises in the context (already marked as
    1.71 +legacy since Isabelle2011).
    1.72  
    1.73  
    1.74  *** HOL ***
    1.75 @@ -184,17 +184,6 @@
    1.76    - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
    1.77      Redefine using other integer operations.
    1.78  
    1.79 -* Records: code generation can be switched off manually with 
    1.80 -declare [[record_coden = false]].  Default remains true.
    1.81 -
    1.82 -* New "case_product" attribute to generate a case rule doing multiple
    1.83 -case distinctions at the same time.  E.g.
    1.84 -
    1.85 -  list.exhaust [case_product nat.exhaust]
    1.86 -
    1.87 -produces a rule which can be used to perform case distinction on both
    1.88 -a list and a nat.
    1.89 -
    1.90  * Transfer: New package intended to generalize the existing
    1.91  "descending" method and related theorem attributes from the Quotient
    1.92  package.  (Not all functionality is implemented yet, but future
    1.93 @@ -336,15 +325,27 @@
    1.94  
    1.95  * Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY.
    1.96  
    1.97 +* New "case_product" attribute to generate a case rule doing multiple
    1.98 +case distinctions at the same time.  E.g.
    1.99 +
   1.100 +  list.exhaust [case_product nat.exhaust]
   1.101 +
   1.102 +produces a rule which can be used to perform case distinction on both
   1.103 +a list and a nat.
   1.104 +
   1.105  * New "eventually_elim" method as a generalized variant of the
   1.106  eventually_elim* rules.  Supports structured proofs.
   1.107  
   1.108 -* 'datatype' specifications allow explicit sort constraints.
   1.109 -
   1.110  * Typedef with implicit set definition is considered legacy.  Use
   1.111  "typedef (open)" form instead, which will eventually become the
   1.112  default.
   1.113  
   1.114 +* Record: code generation can be switched off manually with
   1.115 +
   1.116 +  declare [[record_coden = false]]  -- "default true"
   1.117 +
   1.118 +* Datatype: type parameters allow explicit sort constraints.
   1.119 +
   1.120  * Concrete syntax for case expressions includes constraints for source
   1.121  positions, and thus produces Prover IDE markup for its bindings.
   1.122  INCOMPATIBILITY for old-style syntax translations that augment the
   1.123 @@ -516,15 +517,61 @@
   1.124  * Congruence rules Option.map_cong and Option.bind_cong for recursion
   1.125  through option types.
   1.126  
   1.127 +* "Transitive_Closure.ntrancl": bounded transitive closure on
   1.128 +relations.
   1.129 +
   1.130 +* Constant "Set.not_member" now qualified.  INCOMPATIBILITY.
   1.131 +
   1.132 +* Theory Int: Discontinued many legacy theorems specific to type int.
   1.133 +INCOMPATIBILITY, use the corresponding generic theorems instead.
   1.134 +
   1.135 +  zminus_zminus ~> minus_minus
   1.136 +  zminus_0 ~> minus_zero
   1.137 +  zminus_zadd_distrib ~> minus_add_distrib
   1.138 +  zadd_commute ~> add_commute
   1.139 +  zadd_assoc ~> add_assoc
   1.140 +  zadd_left_commute ~> add_left_commute
   1.141 +  zadd_ac ~> add_ac
   1.142 +  zmult_ac ~> mult_ac
   1.143 +  zadd_0 ~> add_0_left
   1.144 +  zadd_0_right ~> add_0_right
   1.145 +  zadd_zminus_inverse2 ~> left_minus
   1.146 +  zmult_zminus ~> mult_minus_left
   1.147 +  zmult_commute ~> mult_commute
   1.148 +  zmult_assoc ~> mult_assoc
   1.149 +  zadd_zmult_distrib ~> left_distrib
   1.150 +  zadd_zmult_distrib2 ~> right_distrib
   1.151 +  zdiff_zmult_distrib ~> left_diff_distrib
   1.152 +  zdiff_zmult_distrib2 ~> right_diff_distrib
   1.153 +  zmult_1 ~> mult_1_left
   1.154 +  zmult_1_right ~> mult_1_right
   1.155 +  zle_refl ~> order_refl
   1.156 +  zle_trans ~> order_trans
   1.157 +  zle_antisym ~> order_antisym
   1.158 +  zle_linear ~> linorder_linear
   1.159 +  zless_linear ~> linorder_less_linear
   1.160 +  zadd_left_mono ~> add_left_mono
   1.161 +  zadd_strict_right_mono ~> add_strict_right_mono
   1.162 +  zadd_zless_mono ~> add_less_le_mono
   1.163 +  int_0_less_1 ~> zero_less_one
   1.164 +  int_0_neq_1 ~> zero_neq_one
   1.165 +  zless_le ~> less_le
   1.166 +  zpower_zadd_distrib ~> power_add
   1.167 +  zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
   1.168 +  zero_le_zpower_abs ~> zero_le_power_abs
   1.169 +
   1.170 +* Theory Deriv: Renamed
   1.171 +
   1.172 +  DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing
   1.173 +
   1.174 +* Theory Library/Multiset: Improved code generation of multisets.
   1.175 +
   1.176  * Theory HOL/Library/Set_Algebras: Addition and multiplication on sets
   1.177  are expressed via type classes again. The special syntax
   1.178  \<oplus>/\<otimes> has been replaced by plain +/*. Removed constant
   1.179  setsum_set, which is now subsumed by Big_Operators.setsum.
   1.180  INCOMPATIBILITY.
   1.181  
   1.182 -* New theory HOL/Library/DAList provides an abstract type for
   1.183 -association lists with distinct keys.
   1.184 -
   1.185  * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
   1.186  use theory HOL/Library/Nat_Bijection instead.
   1.187  
   1.188 @@ -704,52 +751,8 @@
   1.189    real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,
   1.190    round_up, zero_le_float, zero_less_float
   1.191  
   1.192 -* "Transitive_Closure.ntrancl": bounded transitive closure on
   1.193 -relations.
   1.194 -
   1.195 -* Constant "Set.not_member" now qualified.  INCOMPATIBILITY.
   1.196 -
   1.197 -* Theory Int: Discontinued many legacy theorems specific to type int.
   1.198 -INCOMPATIBILITY, use the corresponding generic theorems instead.
   1.199 -
   1.200 -  zminus_zminus ~> minus_minus
   1.201 -  zminus_0 ~> minus_zero
   1.202 -  zminus_zadd_distrib ~> minus_add_distrib
   1.203 -  zadd_commute ~> add_commute
   1.204 -  zadd_assoc ~> add_assoc
   1.205 -  zadd_left_commute ~> add_left_commute
   1.206 -  zadd_ac ~> add_ac
   1.207 -  zmult_ac ~> mult_ac
   1.208 -  zadd_0 ~> add_0_left
   1.209 -  zadd_0_right ~> add_0_right
   1.210 -  zadd_zminus_inverse2 ~> left_minus
   1.211 -  zmult_zminus ~> mult_minus_left
   1.212 -  zmult_commute ~> mult_commute
   1.213 -  zmult_assoc ~> mult_assoc
   1.214 -  zadd_zmult_distrib ~> left_distrib
   1.215 -  zadd_zmult_distrib2 ~> right_distrib
   1.216 -  zdiff_zmult_distrib ~> left_diff_distrib
   1.217 -  zdiff_zmult_distrib2 ~> right_diff_distrib
   1.218 -  zmult_1 ~> mult_1_left
   1.219 -  zmult_1_right ~> mult_1_right
   1.220 -  zle_refl ~> order_refl
   1.221 -  zle_trans ~> order_trans
   1.222 -  zle_antisym ~> order_antisym
   1.223 -  zle_linear ~> linorder_linear
   1.224 -  zless_linear ~> linorder_less_linear
   1.225 -  zadd_left_mono ~> add_left_mono
   1.226 -  zadd_strict_right_mono ~> add_strict_right_mono
   1.227 -  zadd_zless_mono ~> add_less_le_mono
   1.228 -  int_0_less_1 ~> zero_less_one
   1.229 -  int_0_neq_1 ~> zero_neq_one
   1.230 -  zless_le ~> less_le
   1.231 -  zpower_zadd_distrib ~> power_add
   1.232 -  zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
   1.233 -  zero_le_zpower_abs ~> zero_le_power_abs
   1.234 -
   1.235 -* Theory Deriv: Renamed
   1.236 -
   1.237 -  DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing
   1.238 +* New theory HOL/Library/DAList provides an abstract type for
   1.239 +association lists with distinct keys.
   1.240  
   1.241  * Session HOL-Import: Re-implementation from scratch is faster,
   1.242  simpler, and more scalable.  Requires a proof bundle, which is
   1.243 @@ -802,8 +805,6 @@
   1.244    word_of_int_0_hom ~> word_0_wi
   1.245    word_of_int_1_hom ~> word_1_wi
   1.246  
   1.247 -* Theory Library/Multiset: Improved code generation of multisets.
   1.248 -
   1.249  * Session HOL-Word: New proof method "word_bitwise" for splitting
   1.250  machine word equalities and inequalities into logical circuits,
   1.251  defined in HOL/Word/WordBitwise.thy.  Supports addition, subtraction,
   1.252 @@ -816,9 +817,9 @@
   1.253  * Session HOL-Probability: Introduced the type "'a measure" to
   1.254  represent measures, this replaces the records 'a algebra and 'a
   1.255  measure_space.  The locales based on subset_class now have two
   1.256 -locale-parameters the space \<Omega> and the set of measurable sets
   1.257 -M.  The product of probability spaces uses now the same constant as
   1.258 -the finite product of sigma-finite measure spaces "PiM :: ('i => 'a)
   1.259 +locale-parameters the space \<Omega> and the set of measurable sets M.
   1.260 +The product of probability spaces uses now the same constant as the
   1.261 +finite product of sigma-finite measure spaces "PiM :: ('i => 'a)
   1.262  measure".  Most constants are defined now outside of locales and gain
   1.263  an additional parameter, like null_sets, almost_eventually or \<mu>'.
   1.264  Measure space constructions for distributions and densities now got