equal
deleted
inserted
replaced
73 |
73 |
74 * Session HOL-Word: Compound operation "bin_split" simplifies by default |
74 * Session HOL-Word: Compound operation "bin_split" simplifies by default |
75 into its components "drop_bit" and "take_bit". INCOMPATIBILITY. |
75 into its components "drop_bit" and "take_bit". INCOMPATIBILITY. |
76 |
76 |
77 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth", |
77 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth", |
78 "bintrunc", "sbintrunc", "bin_cat" and "max_word" are now mere |
78 "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now |
79 input abbreviations. Minor INCOMPATIBILITY. |
79 mere input abbreviations. Minor INCOMPATIBILITY. |
80 |
80 |
81 * Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer. |
81 * Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer. |
82 Minor INCOMPATIBILITY. |
82 Minor INCOMPATIBILITY. |
83 |
83 |
84 * Session HOL-Word: Operations lsb, msb and set_bit are separated |
84 * Session HOL-Word: Operations lsb, msb and set_bit are separated |