NEWS
 changeset 16888 7cb4bcfa058e parent 16869 bc98da5727be child 16891 20bd6e8c9a4f
equal inserted replaced
16887:b24c067b32d6 16888:7cb4bcfa058e
`   348 otherwise we unfold the let and arrive at g.  The simproc can be`
`   348 otherwise we unfold the let and arrive at g.  The simproc can be`
`   349 enabled/disabled by the reference use_let_simproc.  Potential`
`   349 enabled/disabled by the reference use_let_simproc.  Potential`
`   350 INCOMPATIBILITY since simplification is more powerful by default.`
`   350 INCOMPATIBILITY since simplification is more powerful by default.`
`   351 `
`   351 `
`   352 * Classical reasoning: the meson method now accepts theorems as arguments.`
`   352 * Classical reasoning: the meson method now accepts theorems as arguments.`
`       `
`   353 `
`       `
`   354 * Introduced various additions and improvements in OrderedGroup.thy and `
`       `
`   355 Ring_and_Field.thy, to faciliate calculations involving equalities `
`       `
`   356 and inequalities.`
`       `
`   357 `
`       `
`   358 * Added rules for simplifying exponents to Parity.thy`
`       `
`   359 `
`       `
`   360 Below are some theorems that have been eliminated or modified in this release:`
`       `
`   361 `
`       `
`   362   abs_eq             now named abs_of_nonneg`
`       `
`   363   abs_of_ge_0        now named abs_of_nonneg `
`       `
`   364   abs_minus_eq       now named abs_of_nonpos  `
`       `
`   365   imp_abs_id         now named abs_of_nonneg`
`       `
`   366   imp_abs_neg_id     now named abs_of_nonpos`
`       `
`   367   mult_pos           now named mult_pos_pos`
`       `
`   368   mult_pos_le        now named mult_nonneg_nonneg`
`       `
`   369   mult_pos_neg_le    now named mult_nonneg_nonpos`
`       `
`   370   mult_pos_neg2_le   now named mult_nonneg_nonpos2`
`       `
`   371   mult_neg           now named mult_neg_neg`
`       `
`   372   mult_neg_le        now named mult_nonpos_nonpos`
`       `
`   373 `
`       `
`   374 `
`       `
`   375 *** HOL-Complex ***`
`       `
`   376 `
`       `
`   377 * Introduced better support for embedding natural numbers and integers`
`       `
`   378 in the reals, in RealDef.thy.`
`       `
`   379 `
`       `
`   380 * Expanded support for floor and ceiling functions, in RComplete.thy.`
`       `
`   381 `
`       `
`   382 Below are some theorems that have been eliminated or modified in this release:`
`       `
`   383 `
`       `
`   384   real_of_int_add    reversed direction of equality (use "THEN sym")`
`       `
`   385   real_of_int_minus  reversed direction of equality (use "THEN sym")`
`       `
`   386   real_of_int_diff   reversed direction of equality (use "THEN sym")`
`       `
`   387   real_of_int_mult   reversed direction of equality (use "THEN sym")`
`   353 `
`   388 `
`   354 `
`   389 `
`   355 *** HOLCF ***`
`   390 *** HOLCF ***`
`   356 `
`   391 `
`   357 * HOLCF: discontinued special version of 'constdefs' (which used to`
`   392 * HOLCF: discontinued special version of 'constdefs' (which used to`