NEWS
changeset 17092 16971afe75f6
parent 17047 e2e2d75bb37b
child 17095 669005f73b81
equal deleted inserted replaced
17091:13593aa6a546 17092:16971afe75f6
   383   mult_pos_neg2_le   now named mult_nonneg_nonpos2
   383   mult_pos_neg2_le   now named mult_nonneg_nonpos2
   384   mult_neg           now named mult_neg_neg
   384   mult_neg           now named mult_neg_neg
   385   mult_neg_le        now named mult_nonpos_nonpos
   385   mult_neg_le        now named mult_nonpos_nonpos
   386 
   386 
   387 * Theory Parity: added rules for simplifying exponents.
   387 * Theory Parity: added rules for simplifying exponents.
       
   388 
       
   389 * Theory List:
       
   390 
       
   391 The following theorems have been eliminated or modified
       
   392 (INCOMPATIBILITY):
       
   393 
       
   394   list_all_Nil       now named list_all.simps(1)
       
   395   list_all_Cons      now named list_all.simps(2)
       
   396   list_all_conv      now named list_all_iff
       
   397   set_mem_eq         now named mem_iff
   388 
   398 
   389 * Theories SetsAndFunctions and BigO (see HOL/Library) support
   399 * Theories SetsAndFunctions and BigO (see HOL/Library) support
   390 asymptotic "big O" calculations.  See the notes in BigO.thy.
   400 asymptotic "big O" calculations.  See the notes in BigO.thy.
   391 
   401 
   392 
   402