NEWS
changeset 36849 33e5b40ec4bb
parent 36848 7e6f334b294b
child 36856 b343091e81d8
equal deleted inserted replaced
36848:7e6f334b294b 36849:33e5b40ec4bb
   147 INCOMPATIBILITY.
   147 INCOMPATIBILITY.
   148 
   148 
   149 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
   149 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
   150 INCOMPATIBILITY.
   150 INCOMPATIBILITY.
   151 
   151 
   152 * Dropped normalizing. Use semiring classes directly. INCOMPATIBILITY.
   152 * Dropped normalizing_semiring etc; use the facts in semiring classes instead.
       
   153 INCOMPATIBILITY.
   153 
   154 
   154 * Theory 'Finite_Set': various folding_* locales facilitate the application
   155 * Theory 'Finite_Set': various folding_* locales facilitate the application
   155 of the various fold combinators on finite sets.
   156 of the various fold combinators on finite sets.
   156 
   157 
   157 * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
   158 * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'