equal
deleted
inserted
replaced
543 * Pure: 'print_theory' now suppresses entities with internal name |
543 * Pure: 'print_theory' now suppresses entities with internal name |
544 (trailing "_") by default; use '!' option for full details. |
544 (trailing "_") by default; use '!' option for full details. |
545 |
545 |
546 |
546 |
547 *** HOL *** |
547 *** HOL *** |
|
548 |
|
549 * IntDef: The constant "int :: nat => int" has been removed; now |
|
550 "int" is an abbreviation for "of_nat :: nat => int". Potential |
|
551 INCOMPATIBILITY due to differences in default simp rules: |
|
552 - "int (Suc m)" simplifies to "int m + 1" instead of "1 + int m" |
|
553 - "int (m * n)" simplifies to "int m * int n" |
548 |
554 |
549 * Method "algebra" solves polynomial equations over (semi)rings using |
555 * Method "algebra" solves polynomial equations over (semi)rings using |
550 Groebner bases. The (semi)ring structure is defined by locales and |
556 Groebner bases. The (semi)ring structure is defined by locales and |
551 the tool setup depends on that generic context. Installing the |
557 the tool setup depends on that generic context. Installing the |
552 method for a specific type involves instantiating the locale and |
558 method for a specific type involves instantiating the locale and |