equal
deleted
inserted
replaced
507 * Dropped old infix syntax "_ mem _" for List.member; use "_ : set _" |
507 * Dropped old infix syntax "_ mem _" for List.member; use "_ : set _" |
508 instead. INCOMPATIBILITY. |
508 instead. INCOMPATIBILITY. |
509 |
509 |
510 * Removed lemma Option.is_none_none (Duplicate of is_none_def). |
510 * Removed lemma Option.is_none_none (Duplicate of is_none_def). |
511 INCOMPATIBILITY. |
511 INCOMPATIBILITY. |
|
512 |
|
513 * New commands to load and prove verification conditions generated by |
|
514 the SPARK Ada program verifier. See src/HOL/SPARK. |
512 |
515 |
513 |
516 |
514 *** HOL-Algebra *** |
517 *** HOL-Algebra *** |
515 |
518 |
516 * Theorems for additive ring operations (locale abelian_monoid and |
519 * Theorems for additive ring operations (locale abelian_monoid and |