equal
deleted
inserted
replaced
514 * Pure: 'print_theory' now suppresses entities with internal name |
514 * Pure: 'print_theory' now suppresses entities with internal name |
515 (trailing "_") by default; use '!' option for full details. |
515 (trailing "_") by default; use '!' option for full details. |
516 |
516 |
517 |
517 |
518 *** HOL *** |
518 *** HOL *** |
|
519 |
|
520 * Internal reorganisation of `size' of datatypes: |
|
521 - size theorems "foo.size" are no longer subsumed by "foo.simps" (but are still |
|
522 simplification rules by default!) |
|
523 - theorems "prod.size" now named "*.size" |
519 |
524 |
520 * The transitivity reasoner for partial and linear orders is set up for |
525 * The transitivity reasoner for partial and linear orders is set up for |
521 locales `order' and `linorder' generated by the new class package. Previously |
526 locales `order' and `linorder' generated by the new class package. Previously |
522 the reasoner was only set up for axiomatic type classes. Instances of the |
527 the reasoner was only set up for axiomatic type classes. Instances of the |
523 reasoner are available in all contexts importing or interpreting these locales. |
528 reasoner are available in all contexts importing or interpreting these locales. |