equal
deleted
inserted
replaced
167 |
167 |
168 * Library theory "Signed_Division" provides operations for signed |
168 * Library theory "Signed_Division" provides operations for signed |
169 division, instantiated for type int. |
169 division, instantiated for type int. |
170 |
170 |
171 * Theory "Multiset": removed misleading notation \<Union># for sum_mset; |
171 * Theory "Multiset": removed misleading notation \<Union># for sum_mset; |
172 replaced with \<Sum>\<^sub>#. |
172 replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also |
|
173 exists now. |
173 |
174 |
174 * Self-contained library theory "Word" taken over from former session |
175 * Self-contained library theory "Word" taken over from former session |
175 "HOL-Word". |
176 "HOL-Word". |
176 |
177 |
177 * Theory "Word": Type word is restricted to bit strings consisting of at |
178 * Theory "Word": Type word is restricted to bit strings consisting of at |