NEWS
changeset 72546 58b1826354c9
parent 72521 354bfab78cbf
child 72557 6345cce0e576
equal deleted inserted replaced
72545:55a50f65c928 72546:58b1826354c9
   145 * Former session "HOL-Word": Compound operation "bin_split" simplifies
   145 * Former session "HOL-Word": Compound operation "bin_split" simplifies
   146 by default into its components "drop_bit" and "take_bit".
   146 by default into its components "drop_bit" and "take_bit".
   147 INCOMPATIBILITY.
   147 INCOMPATIBILITY.
   148 
   148 
   149 * Former session "HOL-Word": Operations lsb, msb and set_bit are
   149 * Former session "HOL-Word": Operations lsb, msb and set_bit are
   150 separated into theories Misc_lsb, Misc_msb and Misc_set_bit respectively
   150 separated into theories Least_significant_bit, Most_significant_bit and
   151 in session Word_Lib in the AFP.  INCOMPATIBILITY.
   151 Generic_set_bit respectively in session Word_Lib in the AFP.
       
   152 INCOMPATIBILITY.
   152 
   153 
   153 * Former session "HOL-Word": Ancient int numeral representation has been
   154 * Former session "HOL-Word": Ancient int numeral representation has been
   154 factored out in separate theory "Ancient_Numeral" in session Word_Lib
   155 factored out in separate theory "Ancient_Numeral" in session Word_Lib
   155 in the AFP.  INCOMPATIBILITY.
   156 in the AFP.  INCOMPATIBILITY.
   156 
   157