changeset 45233 | 28b076e0bea8 |
parent 45210 | b416573f1807 |
child 45293 | 57def0b39696 |
--- a/NEWS Fri Oct 21 11:17:15 2011 +0200 +++ b/NEWS Fri Oct 21 11:17:16 2011 +0200 @@ -13,6 +13,9 @@ 'code_library', 'consts_code', 'types_code' have been discontinued. Use commands of the generic code generator instead. INCOMPATIBILITY. +* Redundant attribute 'code_inline' has been discontinued. Use 'code_unfold' +instead. INCOMPATIBILITY. + *** HOL *** * 'Transitive_Closure.ntrancl': bounded transitive closure on relations.