equal
deleted
inserted
replaced
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 |