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