equal
deleted
inserted
replaced
493 |
493 |
494 * Dropped old infix syntax "_ mem _" for List.member; use "_ : set _" |
494 * Dropped old infix syntax "_ mem _" for List.member; use "_ : set _" |
495 instead. INCOMPATIBILITY. |
495 instead. INCOMPATIBILITY. |
496 |
496 |
497 * Removed lemma Option.is_none_none (Duplicate of is_none_def). |
497 * Removed lemma Option.is_none_none (Duplicate of is_none_def). |
|
498 INCOMPATIBILITY. |
|
499 |
|
500 |
|
501 *** HOL-Algebra *** |
|
502 |
|
503 * Theorems for additive ring operations (locale abelian_monoid and |
|
504 descendants) are generated by interpretation from their multiplicative |
|
505 counterparts. This causes slight differences in the simp and clasets. |
498 INCOMPATIBILITY. |
506 INCOMPATIBILITY. |
499 |
507 |
500 |
508 |
501 *** HOLCF *** |
509 *** HOLCF *** |
502 |
510 |