equal
deleted
inserted
replaced
505 (trailing "_") by default; use '!' option for full details. |
505 (trailing "_") by default; use '!' option for full details. |
506 |
506 |
507 |
507 |
508 *** HOL *** |
508 *** HOL *** |
509 |
509 |
|
510 * Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq. |
|
511 INCOMPATIBILITY. |
|
512 |
|
513 * Dropped lemma duplicate if_def2 in favor of if_bool_eq_conj. |
|
514 INCOMPATIBILITY. |
|
515 |
510 * Added syntactic class "size"; overloaded constant "size" now has |
516 * Added syntactic class "size"; overloaded constant "size" now has |
511 type "'a::size ==> bool" |
517 type "'a::size ==> bool" |
512 |
518 |
513 * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op |
519 * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op |
514 dvd" to "Divides.div", "Divides.mod" and |
520 dvd" to "Divides.div", "Divides.mod" and "Divides.dvd" |
515 "Divides.dvd". INCOMPATIBILITY. |
521 "Divides.dvd". INCOMPATIBILITY. |
516 |
522 |
517 * Added method "lexicographic_order" automatically synthesizes |
523 * Added method "lexicographic_order" automatically synthesizes |
518 termination relations as lexicographic combinations of size measures |
524 termination relations as lexicographic combinations of size measures |
519 -- 'function' package. |
525 -- 'function' package. |