1.1 --- a/NEWS Wed May 02 20:15:31 2012 +0200
1.2 +++ b/NEWS Wed May 02 20:31:15 2012 +0200
1.3 @@ -47,10 +47,8 @@
1.4 * Bundled declarations associate attributed fact expressions with a
1.5 given name in the context. These may be later included in other
1.6 contexts. This allows to manage context extensions casually, without
1.7 -the logical dependencies of locales and locale interpretation.
1.8 -
1.9 -See commands 'bundle', 'include', 'including' etc. in the isar-ref
1.10 -manual.
1.11 +the logical dependencies of locales and locale interpretation. See
1.12 +commands 'bundle', 'include', 'including' etc. in the isar-ref manual.
1.13
1.14 * Commands 'lemmas' and 'theorems' allow local variables using 'for'
1.15 declaration, and results are standardized before being stored. Thus
1.16 @@ -91,25 +89,25 @@
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
1.20 -* Renamed some inner syntax categories:
1.21 -
1.22 - num ~> num_token
1.23 - xnum ~> xnum_token
1.24 - xstr ~> str_token
1.25 -
1.26 -Minor INCOMPATIBILITY. Note that in practice "num_const" or
1.27 -"num_position" etc. are mainly used instead (which also include
1.28 -position information via constraints).
1.29 -
1.30 -* Simplified configuration options for syntax ambiguity: see
1.31 -"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
1.32 -manual. Minor INCOMPATIBILITY.
1.33 -
1.34 * Attribute "abs_def" turns an equation of the form "f x y == t" into
1.35 "f == %x y. t", which ensures that "simp" or "unfold" steps always
1.36 expand it. This also works for object-logic equality. (Formerly
1.37 undocumented feature.)
1.38
1.39 +* Renamed some inner syntax categories:
1.40 +
1.41 + num ~> num_token
1.42 + xnum ~> xnum_token
1.43 + xstr ~> str_token
1.44 +
1.45 +Minor INCOMPATIBILITY. Note that in practice "num_const" or
1.46 +"num_position" etc. are mainly used instead (which also include
1.47 +position information via constraints).
1.48 +
1.49 +* Simplified configuration options for syntax ambiguity: see
1.50 +"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
1.51 +manual. Minor INCOMPATIBILITY.
1.52 +
1.53 * Obsolete command 'types' has been discontinued. Use 'type_synonym'
1.54 instead. INCOMPATIBILITY.
1.55
1.56 @@ -136,29 +134,38 @@
1.57 lemma "P (x::'a)" and "Q (y::'a::bar)"
1.58 -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
1.59
1.60 +* Discontinued configuration option "syntax_positions": atomic terms
1.61 +in parse trees are always annotated by position constraints.
1.62 +
1.63
1.64 *** HOL ***
1.65
1.66 * Type 'a set is now a proper type constructor (just as before
1.67 Isabelle2008). Definitions mem_def and Collect_def have disappeared.
1.68 Non-trivial INCOMPATIBILITY. For developments keeping predicates and
1.69 -sets separate, it is often sufficient to rephrase sets S accidentally
1.70 -used as predicates by "%x. x : S" and predicates P accidentally used
1.71 -as sets by "{x. P x}". Corresponding proofs in a first step should be
1.72 -pruned from any tinkering with former theorems mem_def and Collect_def
1.73 -as far as possible.
1.74 -
1.75 -For developments which deliberately mixed predicates and sets, a
1.76 +sets separate, it is often sufficient to rephrase some set S that has
1.77 +been accidentally used as predicates by "%x. x : S", and some
1.78 +predicate P that has been accidentally used as set by "{x. P x}".
1.79 +Corresponding proofs in a first step should be pruned from any
1.80 +tinkering with former theorems mem_def and Collect_def as far as
1.81 +possible.
1.82 +
1.83 +For developments which deliberately mix predicates and sets, a
1.84 planning step is necessary to determine what should become a predicate
1.85 and what a set. It can be helpful to carry out that step in
1.86 Isabelle2011-1 before jumping right into the current release.
1.87
1.88 +* Code generation by default implements sets as container type rather
1.89 +than predicates. INCOMPATIBILITY.
1.90 +
1.91 +* New type synonym 'a rel = ('a * 'a) set
1.92 +
1.93 * The representation of numerals has changed. Datatype "num"
1.94 represents strictly positive binary numerals, along with functions
1.95 "numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent
1.96 -positive and negated numeric literals, respectively. (See definitions
1.97 -in ~~/src/HOL/Num.thy.) Potential INCOMPATIBILITY, some user theories
1.98 -may require adaptations as follows:
1.99 +positive and negated numeric literals, respectively. See also
1.100 +definitions in ~~/src/HOL/Num.thy. Potential INCOMPATIBILITY, some
1.101 +user theories may require adaptations as follows:
1.102
1.103 - Theorems with number_ring or number_semiring constraints: These
1.104 classes are gone; use comm_ring_1 or comm_semiring_1 instead.
1.105 @@ -177,18 +184,8 @@
1.106 - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
1.107 Redefine using other integer operations.
1.108
1.109 -* Code generation by default implements sets as container type rather
1.110 -than predicates. INCOMPATIBILITY.
1.111 -
1.112 * Records: code generation can be switched off manually with
1.113 -declare [[record_coden = false]]. Default remains true.
1.114 -
1.115 -* HOL-Import: Re-implementation from scratch is faster, simpler, and
1.116 -more scalable. Requires a proof bundle, which is available as an
1.117 -external component. Discontinued old (and mostly dead) Importer for
1.118 -HOL4 and HOL Light. INCOMPATIBILITY.
1.119 -
1.120 -* New type synonym 'a rel = ('a * 'a) set
1.121 +declare [[record_coden = false]]. Default remains true.
1.122
1.123 * New "case_product" attribute to generate a case rule doing multiple
1.124 case distinctions at the same time. E.g.
1.125 @@ -198,11 +195,11 @@
1.126 produces a rule which can be used to perform case distinction on both
1.127 a list and a nat.
1.128
1.129 -* Transfer: New package intended to generalize the existing descending
1.130 -method and related theorem attributes from the Quotient package. (Not
1.131 -all functionality is implemented yet, but future development will
1.132 -focus on Transfer as an eventual replacement for the corresponding
1.133 -parts of the Quotient package.)
1.134 +* Transfer: New package intended to generalize the existing
1.135 +"descending" method and related theorem attributes from the Quotient
1.136 +package. (Not all functionality is implemented yet, but future
1.137 +development will focus on Transfer as an eventual replacement for the
1.138 +corresponding parts of the Quotient package.)
1.139
1.140 - transfer_rule attribute: Maintains a collection of transfer rules,
1.141 which relate constants at two different types. Transfer rules may
1.142 @@ -218,7 +215,7 @@
1.143 replaced with corresponding ones according to the transfer rules.
1.144 Goals are generalized over all free variables by default; this is
1.145 necessary for variables whose types change, but can be overridden
1.146 - for specific variables with e.g. 'transfer fixing: x y z'. The
1.147 + for specific variables with e.g. "transfer fixing: x y z". The
1.148 variant transfer' method allows replacing a subgoal with one that
1.149 is logically stronger (rather than equivalent).
1.150
1.151 @@ -317,9 +314,8 @@
1.152 - Added "quickcheck_locale" configuration to specify how to process
1.153 conjectures in a locale context.
1.154
1.155 -* Nitpick:
1.156 - - Fixed infinite loop caused by the 'peephole_optim' option and
1.157 - affecting 'rat' and 'real'.
1.158 +* Nitpick: Fixed infinite loop caused by the 'peephole_optim' option
1.159 +and affecting 'rat' and 'real'.
1.160
1.161 * Sledgehammer:
1.162 - Integrated more tightly with SPASS, as described in the ITP 2012
1.163 @@ -333,23 +329,31 @@
1.164 - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
1.165 - Renamed "sound" option to "strict".
1.166
1.167 -* Metis:
1.168 - - Added possibility to specify lambda translations scheme as a
1.169 - parenthesized argument (e.g., "by (metis (lifting) ...)").
1.170 -
1.171 -* SMT:
1.172 - - Renamed "smt_fixed" option to "smt_read_only_certificates".
1.173 -
1.174 -* Command 'try0':
1.175 - - Renamed from 'try_methods'. INCOMPATIBILITY.
1.176 +* Metis: Added possibility to specify lambda translations scheme as a
1.177 +parenthesized argument (e.g., "by (metis (lifting) ...)").
1.178 +
1.179 +* SMT: Renamed "smt_fixed" option to "smt_read_only_certificates".
1.180 +
1.181 +* Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY.
1.182
1.183 * New "eventually_elim" method as a generalized variant of the
1.184 -eventually_elim* rules. Supports structured proofs.
1.185 +eventually_elim* rules. Supports structured proofs.
1.186 +
1.187 +* 'datatype' specifications allow explicit sort constraints.
1.188
1.189 * Typedef with implicit set definition is considered legacy. Use
1.190 "typedef (open)" form instead, which will eventually become the
1.191 default.
1.192
1.193 +* Concrete syntax for case expressions includes constraints for source
1.194 +positions, and thus produces Prover IDE markup for its bindings.
1.195 +INCOMPATIBILITY for old-style syntax translations that augment the
1.196 +pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
1.197 +one_case.
1.198 +
1.199 +* Clarified attribute "mono_set": pure declaration without modifying
1.200 +the result of the fact expression.
1.201 +
1.202 * More default pred/set conversions on a couple of relation operations
1.203 and predicates. Added powers of predicate relations. Consolidation
1.204 of some relation theorems:
1.205 @@ -512,16 +516,7 @@
1.206 * Congruence rules Option.map_cong and Option.bind_cong for recursion
1.207 through option types.
1.208
1.209 -* Concrete syntax for case expressions includes constraints for source
1.210 -positions, and thus produces Prover IDE markup for its bindings.
1.211 -INCOMPATIBILITY for old-style syntax translations that augment the
1.212 -pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
1.213 -one_case.
1.214 -
1.215 -* Discontinued configuration option "syntax_positions": atomic terms
1.216 -in parse trees are always annotated by position constraints.
1.217 -
1.218 -* HOL/Library/Set_Algebras.thy: Addition and multiplication on sets
1.219 +* Theory HOL/Library/Set_Algebras: Addition and multiplication on sets
1.220 are expressed via type classes again. The special syntax
1.221 \<oplus>/\<otimes> has been replaced by plain +/*. Removed constant
1.222 setsum_set, which is now subsumed by Big_Operators.setsum.
1.223 @@ -530,8 +525,6 @@
1.224 * New theory HOL/Library/DAList provides an abstract type for
1.225 association lists with distinct keys.
1.226
1.227 -* 'datatype' specifications allow explicit sort constraints.
1.228 -
1.229 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
1.230 use theory HOL/Library/Nat_Bijection instead.
1.231
1.232 @@ -711,6 +704,58 @@
1.233 real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,
1.234 round_up, zero_le_float, zero_less_float
1.235
1.236 +* "Transitive_Closure.ntrancl": bounded transitive closure on
1.237 +relations.
1.238 +
1.239 +* Constant "Set.not_member" now qualified. INCOMPATIBILITY.
1.240 +
1.241 +* Theory Int: Discontinued many legacy theorems specific to type int.
1.242 +INCOMPATIBILITY, use the corresponding generic theorems instead.
1.243 +
1.244 + zminus_zminus ~> minus_minus
1.245 + zminus_0 ~> minus_zero
1.246 + zminus_zadd_distrib ~> minus_add_distrib
1.247 + zadd_commute ~> add_commute
1.248 + zadd_assoc ~> add_assoc
1.249 + zadd_left_commute ~> add_left_commute
1.250 + zadd_ac ~> add_ac
1.251 + zmult_ac ~> mult_ac
1.252 + zadd_0 ~> add_0_left
1.253 + zadd_0_right ~> add_0_right
1.254 + zadd_zminus_inverse2 ~> left_minus
1.255 + zmult_zminus ~> mult_minus_left
1.256 + zmult_commute ~> mult_commute
1.257 + zmult_assoc ~> mult_assoc
1.258 + zadd_zmult_distrib ~> left_distrib
1.259 + zadd_zmult_distrib2 ~> right_distrib
1.260 + zdiff_zmult_distrib ~> left_diff_distrib
1.261 + zdiff_zmult_distrib2 ~> right_diff_distrib
1.262 + zmult_1 ~> mult_1_left
1.263 + zmult_1_right ~> mult_1_right
1.264 + zle_refl ~> order_refl
1.265 + zle_trans ~> order_trans
1.266 + zle_antisym ~> order_antisym
1.267 + zle_linear ~> linorder_linear
1.268 + zless_linear ~> linorder_less_linear
1.269 + zadd_left_mono ~> add_left_mono
1.270 + zadd_strict_right_mono ~> add_strict_right_mono
1.271 + zadd_zless_mono ~> add_less_le_mono
1.272 + int_0_less_1 ~> zero_less_one
1.273 + int_0_neq_1 ~> zero_neq_one
1.274 + zless_le ~> less_le
1.275 + zpower_zadd_distrib ~> power_add
1.276 + zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
1.277 + zero_le_zpower_abs ~> zero_le_power_abs
1.278 +
1.279 +* Theory Deriv: Renamed
1.280 +
1.281 + DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing
1.282 +
1.283 +* Session HOL-Import: Re-implementation from scratch is faster,
1.284 +simpler, and more scalable. Requires a proof bundle, which is
1.285 +available as an external component. Discontinued old (and mostly
1.286 +dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY.
1.287 +
1.288 * Session HOL-Word: Discontinued many redundant theorems specific to
1.289 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
1.290 instead.
1.291 @@ -757,56 +802,6 @@
1.292 word_of_int_0_hom ~> word_0_wi
1.293 word_of_int_1_hom ~> word_1_wi
1.294
1.295 -* Clarified attribute "mono_set": pure declaration without modifying
1.296 -the result of the fact expression.
1.297 -
1.298 -* "Transitive_Closure.ntrancl": bounded transitive closure on
1.299 -relations.
1.300 -
1.301 -* Constant "Set.not_member" now qualified. INCOMPATIBILITY.
1.302 -
1.303 -* Theory Int: Discontinued many legacy theorems specific to type int.
1.304 -INCOMPATIBILITY, use the corresponding generic theorems instead.
1.305 -
1.306 - zminus_zminus ~> minus_minus
1.307 - zminus_0 ~> minus_zero
1.308 - zminus_zadd_distrib ~> minus_add_distrib
1.309 - zadd_commute ~> add_commute
1.310 - zadd_assoc ~> add_assoc
1.311 - zadd_left_commute ~> add_left_commute
1.312 - zadd_ac ~> add_ac
1.313 - zmult_ac ~> mult_ac
1.314 - zadd_0 ~> add_0_left
1.315 - zadd_0_right ~> add_0_right
1.316 - zadd_zminus_inverse2 ~> left_minus
1.317 - zmult_zminus ~> mult_minus_left
1.318 - zmult_commute ~> mult_commute
1.319 - zmult_assoc ~> mult_assoc
1.320 - zadd_zmult_distrib ~> left_distrib
1.321 - zadd_zmult_distrib2 ~> right_distrib
1.322 - zdiff_zmult_distrib ~> left_diff_distrib
1.323 - zdiff_zmult_distrib2 ~> right_diff_distrib
1.324 - zmult_1 ~> mult_1_left
1.325 - zmult_1_right ~> mult_1_right
1.326 - zle_refl ~> order_refl
1.327 - zle_trans ~> order_trans
1.328 - zle_antisym ~> order_antisym
1.329 - zle_linear ~> linorder_linear
1.330 - zless_linear ~> linorder_less_linear
1.331 - zadd_left_mono ~> add_left_mono
1.332 - zadd_strict_right_mono ~> add_strict_right_mono
1.333 - zadd_zless_mono ~> add_less_le_mono
1.334 - int_0_less_1 ~> zero_less_one
1.335 - int_0_neq_1 ~> zero_neq_one
1.336 - zless_le ~> less_le
1.337 - zpower_zadd_distrib ~> power_add
1.338 - zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
1.339 - zero_le_zpower_abs ~> zero_le_power_abs
1.340 -
1.341 -* Theory Deriv: Renamed
1.342 -
1.343 - DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing
1.344 -
1.345 * Theory Library/Multiset: Improved code generation of multisets.
1.346
1.347 * Session HOL-Word: New proof method "word_bitwise" for splitting
1.348 @@ -991,8 +986,8 @@
1.349 sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
1.350 space_product_algebra -> space_PiM
1.351
1.352 -* HOL/TPTP: support to parse and import TPTP problems (all languages)
1.353 -into Isabelle/HOL.
1.354 +* Session HOL-TPTP: support to parse and import TPTP problems (all
1.355 +languages) into Isabelle/HOL.
1.356
1.357
1.358 *** FOL ***