NEWS
changeset 72263 c0a552515c29
parent 72249 4bf8a8a2d2ad
child 72264 47253b1a31ed
equal deleted inserted replaced
72262:a282abb07642 72263:c0a552515c29
    90 generic algebraic bit operations from HOL-Library.Bit_Operations.
    90 generic algebraic bit operations from HOL-Library.Bit_Operations.
    91 INCOMPATIBILITY.
    91 INCOMPATIBILITY.
    92 
    92 
    93 * Session HOL-Word: Most operations on type word are set up
    93 * Session HOL-Word: Most operations on type word are set up
    94 for transfer and lifting.  INCOMPATIBILITY.
    94 for transfer and lifting.  INCOMPATIBILITY.
       
    95 
       
    96 * Session HOL-Word: Generic type conversions.  INCOMPATIBILITY,
       
    97 sometimes additional rewrite rules must be added to applications to
       
    98 get a confluent system again.
    95 
    99 
    96 * Session HOL-Word: Theory "Word_Bitwise" has been moved to AFP entry
   100 * Session HOL-Word: Theory "Word_Bitwise" has been moved to AFP entry
    97 Word_Lib as theory "Bitwise".  INCOMPATIBILITY.
   101 Word_Lib as theory "Bitwise".  INCOMPATIBILITY.
    98 
   102 
    99 * Session HOL-Word: Misc ancient material has been factored out into
   103 * Session HOL-Word: Misc ancient material has been factored out into