equal
deleted
inserted
replaced
46 |
46 |
47 * Added the "at most 1" quantifier, Uniq. |
47 * Added the "at most 1" quantifier, Uniq. |
48 |
48 |
49 * For the natural numbers, Sup {} = 0. |
49 * For the natural numbers, Sup {} = 0. |
50 |
50 |
|
51 * Library theory "Bit_Operations" with generic bit operations. |
|
52 |
|
53 * Session HOL-Word: Bit operations are based on library |
|
54 theory "Bit_Operations". INCOMPATIBILITY. |
|
55 |
|
56 * Session HOL-Word: Compound operation "bin_split" simplifies by default |
|
57 into its components "drop_bit" and "take_bit". INCOMPATIBILITY. |
|
58 |
51 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth", |
59 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth", |
52 "bintrunc" and "max_word" are now mere input abbreviations. |
60 "bintrunc" and "max_word" are now mere input abbreviations. |
53 Minor INCOMPATIBILITY. |
61 Minor INCOMPATIBILITY. |
54 |
|
55 * Session HOL-Word: Compound operation "bin_split" simplifies by default |
|
56 into its components "drop_bit" and "take_bit". INCOMPATIBILITY. |
|
57 |
62 |
58 |
63 |
59 *** FOL *** |
64 *** FOL *** |
60 |
65 |
61 * Added the "at most 1" quantifier, Uniq, as in HOL. |
66 * Added the "at most 1" quantifier, Uniq, as in HOL. |