equal
deleted
inserted
replaced
484 * Pure: 'print_theory' now suppresses entities with internal name |
484 * Pure: 'print_theory' now suppresses entities with internal name |
485 (trailing "_") by default; use '!' option for full details. |
485 (trailing "_") by default; use '!' option for full details. |
486 |
486 |
487 |
487 |
488 *** HOL *** |
488 *** HOL *** |
|
489 |
|
490 * New syntactic class "size"; overloaded constant "size" now |
|
491 has type "'a::size ==> bool" |
|
492 |
|
493 * Constants "Divides.op div", "Divides.op mod" and "Divides.op dvd" no named |
|
494 "Divides.div", "Divides.mod" and "Divides.dvd" |
|
495 INCOMPATIBILITY for ML code directly refering to constant names. |
489 |
496 |
490 * Replaced "auto_term" by the conceptually simpler method "relation", |
497 * Replaced "auto_term" by the conceptually simpler method "relation", |
491 which just applies the instantiated termination rule with no further |
498 which just applies the instantiated termination rule with no further |
492 simplifications. |
499 simplifications. |
493 INCOMPATIBILITY: |
500 INCOMPATIBILITY: |