equal
deleted
inserted
replaced
65 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
65 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
66 token category instead. |
66 token category instead. |
67 |
67 |
68 |
68 |
69 *** HOL *** |
69 *** HOL *** |
|
70 |
|
71 * removed functions "natfloor" and "natceiling", |
|
72 use "nat o floor" and "nat o ceiling" instead. |
|
73 A few of the lemmas have been retained and adapted: in their names |
|
74 "natfloor"/"natceiling" has been replaced by "nat_floor"/"nat_ceiling". |
70 |
75 |
71 * Qualified some duplicated fact names required for boostrapping |
76 * Qualified some duplicated fact names required for boostrapping |
72 the type class hierarchy: |
77 the type class hierarchy: |
73 ab_add_uminus_conv_diff ~> diff_conv_add_uminus |
78 ab_add_uminus_conv_diff ~> diff_conv_add_uminus |
74 field_inverse_zero ~> inverse_zero |
79 field_inverse_zero ~> inverse_zero |