NEWS
changeset 16888 7cb4bcfa058e
parent 16869 bc98da5727be
child 16891 20bd6e8c9a4f
equal deleted 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