equal
deleted
inserted
replaced
473 union_is_rbt -> rbt_union_is_rbt |
473 union_is_rbt -> rbt_union_is_rbt |
474 unionw_is_rbt -> rbt_unionw_is_rbt |
474 unionw_is_rbt -> rbt_unionw_is_rbt |
475 unionwk_is_rbt -> rbt_unionwk_is_rbt |
475 unionwk_is_rbt -> rbt_unionwk_is_rbt |
476 unionwk_sorted -> rbt_unionwk_rbt_sorted |
476 unionwk_sorted -> rbt_unionwk_rbt_sorted |
477 |
477 |
|
478 * Theory HOL/Library/Float: Floating point numbers are now defined as a |
|
479 subset of the real numbers. All operations are defined using the |
|
480 lifing-framework and most proofs use the transfer method. |
|
481 INCOMPATIBILITY. |
|
482 |
|
483 Changed Operations: |
|
484 scale ~> exponent |
|
485 pow2 x ~> use "2 powr (real x)" |
|
486 |
478 * Session HOL-Word: Discontinued many redundant theorems specific to |
487 * Session HOL-Word: Discontinued many redundant theorems specific to |
479 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems |
488 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems |
480 instead. |
489 instead. |
481 |
490 |
482 word_sub_alt ~> word_sub_wi |
491 word_sub_alt ~> word_sub_wi |