81 factored out in separate theory "Ancient_Numeral". INCOMPATIBILITY. |
81 factored out in separate theory "Ancient_Numeral". INCOMPATIBILITY. |
82 |
82 |
83 * Session HOL-Word: Compound operation "bin_split" simplifies by default |
83 * Session HOL-Word: Compound operation "bin_split" simplifies by default |
84 into its components "drop_bit" and "take_bit". INCOMPATIBILITY. |
84 into its components "drop_bit" and "take_bit". INCOMPATIBILITY. |
85 |
85 |
|
86 * Session HOL-Word: Uniform polymorphic "mask" operation for both |
|
87 types int and word. INCOMPATIBILITY |
|
88 |
|
89 * Session HOL-Word: Operations lsb, msb and set_bit are separated |
|
90 into theories Misc_lsb, Misc_msb and Misc_set_bit respectively. |
|
91 INCOMPATIBILITY. |
|
92 |
86 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth", |
93 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth", |
87 "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now |
94 "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now |
88 mere input abbreviations. Minor INCOMPATIBILITY. |
95 mere input abbreviations. Minor INCOMPATIBILITY. |
89 |
96 |
90 * Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer. |
97 * Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer. |
91 Minor INCOMPATIBILITY. |
98 Minor INCOMPATIBILITY. |
92 |
|
93 * Session HOL-Word: Operations lsb, msb and set_bit are separated |
|
94 into theories Misc_lsb, Misc_msb and Misc_set_bit respectively. |
|
95 INCOMPATIBILITY. |
|
96 |
99 |
97 * Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands |
100 * Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands |
98 are in working order again, as opposed to outputting "GaveUp" on nearly |
101 are in working order again, as opposed to outputting "GaveUp" on nearly |
99 all problems. |
102 all problems. |
100 |
103 |