NEWS
changeset 73047 ab9e27da0e85
parent 73009 56eae6d161db
child 73051 6ba08ec184a1
equal deleted inserted replaced
73046:32edc2b4e243 73047:ab9e27da0e85
   159 
   159 
   160 * Library theory "Bit_Operations" with generic bit operations.
   160 * Library theory "Bit_Operations" with generic bit operations.
   161 
   161 
   162 * Library theory "Signed_Division" provides operations for signed
   162 * Library theory "Signed_Division" provides operations for signed
   163 division, instantiated for type int.
   163 division, instantiated for type int.
       
   164 
       
   165 * Theory "Multiset": removed misleading notation \<Union># for sum_mset;
       
   166 replaced with \<Sum>\<^sub>#.
   164 
   167 
   165 * Self-contained library theory "Word" taken over from former session
   168 * Self-contained library theory "Word" taken over from former session
   166 "HOL-Word".
   169 "HOL-Word".
   167 
   170 
   168 * Theory "Word": Type word is restricted to bit strings consisting of at
   171 * Theory "Word": Type word is restricted to bit strings consisting of at