NEWS
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.