equal
deleted
inserted
replaced
273 |
273 |
274 facts |
274 facts |
275 mem_iff ~> member_def |
275 mem_iff ~> member_def |
276 null_empty ~> null_def |
276 null_empty ~> null_def |
277 |
277 |
278 INCOMPATIBILITY. Note that these were not suppossed to be used |
278 INCOMPATIBILITY. Note that these were not supposed to be used |
279 regularly unless for striking reasons; their main purpose was code |
279 regularly unless for striking reasons; their main purpose was code |
280 generation. |
280 generation. |
281 |
281 |
282 * Some previously unqualified names have been qualified: |
282 * Some previously unqualified names have been qualified: |
283 |
283 |
498 * The syntax 'REP('a)' has been replaced with 'DEFL('a)'. |
498 * The syntax 'REP('a)' has been replaced with 'DEFL('a)'. |
499 |
499 |
500 * The predicate 'directed' has been removed. INCOMPATIBILITY. |
500 * The predicate 'directed' has been removed. INCOMPATIBILITY. |
501 |
501 |
502 * The type class 'finite_po' has been removed. INCOMPATIBILITY. |
502 * The type class 'finite_po' has been removed. INCOMPATIBILITY. |
|
503 |
|
504 * The function 'cprod_map' has been renamed to 'prod_map'. |
503 |
505 |
504 * Renamed some theorems (the original names are also still available). |
506 * Renamed some theorems (the original names are also still available). |
505 expand_fun_below ~> fun_below_iff |
507 expand_fun_below ~> fun_below_iff |
506 below_fun_ext ~> fun_belowI |
508 below_fun_ext ~> fun_belowI |
507 expand_cfun_eq ~> cfun_eq_iff |
509 expand_cfun_eq ~> cfun_eq_iff |